<!DOCTYPE html>
<html>
<head>
  <meta http-equiv="content-type" content="text/html; charset=UTF-8" />
  <meta name="generator" content="Madoko, version 0.8.1-beta" />
  <meta name="viewport" content="initial-scale=1.0" />
  <meta name="author" content="Thomas Ball, Jakub Daniel" />
  <title>Deconstructing Dynamic Symbolic Execution</title>
  <style>
/* ---------------------------------------------------
   Various settings to display madoko elements correctly.
   For example, lines in tables or a table of contents.

   All rules use specific madoko classes and never just
   a generic element. This means one can safely include
   this CSS into any web page without affecting non-madoko
   content.
----------------------------------------------------*/

/* The table of contents */
.madoko .toc>.tocblock .tocblock .tocblock {
  margin-left: 2.5em;
}

.madoko .toc>.tocblock .tocblock {
  margin-left: 1.7em;
}

.madoko .toc>.tocblock>.tocitem {
  font-weight: bold;
}

.madoko .toc {
  margin-top: 1em;
}

/* Paragraphs */
.madoko p.para-continue {
  margin-bottom: 0pt;
}

.madoko .para-block+p {
  margin-top: 0pt;
}

.madoko ul.para-block, .madoko ol.para-block {
  margin-top: 0pt;
  margin-bottom: 0pt;
}

.madoko ul.para-end, .madoko ol.para-end {
  margin-bottom: 1em;
}

.madoko dl {
  margin-left: 0em;
}

/* Local page links do not get an underline unless hovering */
.madoko a.localref {
  text-decoration: none;
}
.madoko a.localref:hover {
  text-decoration: underline;
}

/* Footnotes */
.madoko .footnotes {
  font-size: smaller;
  margin-top: 2em;
}

.madoko .footnotes hr {
  width: 50%;
  text-align: left;
}

.madoko .footnote { 
  margin-left: 1em;
}
.madoko .footnote-before {
  margin-left: -1em;
  width: 1em;
  display: inline-block;
}

/* Abstract */
.madoko .abstract>p:first-child:before {
  content: "Abstract. ";
  font-weight: bold;
}

.madoko .abstract {
  margin-left: 2.7em;
  margin-right: 2.7em;
  font-size: small;
}


/* Alignment */
.madoko .align-center, .madoko .align-center>p {
  text-align: center !important;
}

.madoko .align-center pre {
  text-align: left;
}

.madoko .align-center>* {
  margin-left: auto !important;
  margin-right: auto !important;
}

.madoko .align-left, .madoko .align-left>p {
  text-align: left !important;
}

.madoko .align-left>* {
  margin-left: 0pt !important;
  margin-right: auto !important;
}

.madoko .align-right, .madoko .align-right>p {
  text-align: right !important;
}

.madoko .align-right>* {
  margin-left: auto !important;
  margin-right: 0pt !important;
}

.madoko .align-center>table,
.madoko .align-left>table,
.madoko .align-right>table {
  text-align: left !important;
}


/* Equations, Figure's etc. */
.madoko .equation-before {
  float: right;
}


/* Bibliography */
.madoko .bibitem {
  font-size: smaller;
}

.madoko .bib-numeric .bibitem {
  margin-left: 3em;
  text-indent: -3em;
}

.madoko .bibitem-before {
  display: none;
}

.madoko .bib-numeric .bibitem-before {
  display: inline-block;
  width: 3em;
  text-align: right;
}

.madoko .bibliography {
}

.madoko .bibsearch {
  font-size: x-small;
  text-decoration:none;
  color: black;
  font-family: "Segoe UI Symbol", Symbola;
}

/* General */
.madoko .block, .madoko .figure, .madoko .bibitem, .madoko .equation {
  margin-top: 1ex;
  margin-bottom: 1ex;
}

.madoko .figure {
  padding: 0.5em;
  margin-left: 0pt;
  margin-right: 0pt;
}

.madoko .hidden {
  display: none;
}

.madoko .invisible {
  visibility: hidden;
}

.madoko.preview .invisible {
  visibility: visible;
  opacity: 0.5;
}
.madoko.preview[data-view=full] .invisible {
  visibility: hidden;
}

.madoko code.code, .madoko span.code {
  white-space: pre-wrap;
}

.madoko hr, hr.madoko {
  border: none;
  border-bottom: black solid 1px;
  margin-bottom: 0.5ex;
}

.madoko .framed>*:first-child {
  margin-top: 0pt;
}
.madoko .framed>*:last-child {
  margin-bottom: 0pt;
}


/* Title, authors */
.madoko .title {
  font-size: xx-large;
  font-weight: bold;
  margin-bottom: 1ex;
}

.madoko .subtitle {
  font-size: x-large;
  margin-bottom: 1ex;
  margin-top: -1ex;
}

.madoko .titleblock>* {
  margin-left: auto;
  margin-right: auto;
  text-align: center;
}

.madoko .titleblock table {
  width: 80%;
}

.madoko .authorblock .author {
  font-size: large;
}

.madoko .titlenote {
  margin-top: -0.5ex;
  margin-bottom: 1.5ex;
}

/* Lists */

.madoko ul.list-star {
  list-style-type: disc;
}

.madoko ul.list-dash {
    list-style-type: none !important;
}

.madoko ul.list-dash > li:before {
    content: "\2013"; 
    position: absolute;
    margin-left: -1em; 
}

.madoko ul.list-plus {
  list-style-type: square;
}

/* Tables */
.madoko table.madoko {
  border-collapse: collapse;
}
.madoko td, .madoko th {
  padding: 0ex 0.5ex;
  margin: 0pt;
  vertical-align: top;
}

.madoko .cell-border-left {
  border-left: 1px solid black;
}
.madoko .cell-border-right {
  border-right: 1px solid black;
}


.madoko thead>tr:first-child>.cell-line,
.madoko tbody:first-child>tr:first-child>.cell-line {
  border-top: 1px solid black;
  border-bottom: none;
}

.madoko .cell-line, .madoko .cell-double-line {
  border-bottom: 1px solid black;
  border-top: none;
}

.madoko .cell-double-line {
  border-top: 1px solid black;
  padding-top: 1.5px !important;
}


/* Math Pre */
.madoko .input-mathpre .MathJax_Display, .madoko .input-mathpre .math-display {
  text-align: left !important;
}

.madoko div.input-mathpre {
  margin-top: 1.5ex;
  margin-bottom: 1ex;
}

.madoko .math-rendering {
  color: gray;
}


/*---------------------------------------------------------------------------
  Default style for syntax highlighting
---------------------------------------------------------------------------*/

.highlighted                        { color: black; }
.highlighted .token.identifier      { }
.highlighted .token.operators       { }
.highlighted .token.keyword         { color: blue }
.highlighted .token.string          { color: maroon } 
.highlighted .token.string.escape   { color: gray }
.highlighted .token.comment         { color: darkgreen }
.highlighted .token.comment.doc     { font-style: normal }
.highlighted .token.constant        { color: purple; }
.highlighted .token.entity          {  }
.highlighted .token.tag             { color: blue }
.highlighted .token.info-token      { color: black }
.highlighted .token.warn-token      { color: black }
.highlighted .token.error-token     { color: darkred }
.highlighted .token.debug-token     { color: gray }
.highlighted .token.regexp          { color: maroon }
.highlighted .token.attribute.name  { color: navy }
.highlighted .token.attribute.value { color: maroon }
.highlighted .token.constructor     { color: purple }
.highlighted .token.namespace       { color: navy }
.highlighted .token.header          { color: navy }
.highlighted .token.type            { color: teal } 
.highlighted .token.type.delimiter  { color: teal; } 
.highlighted .token.predefined      { color: navy }
.highlighted .token.invalid         { border-bottom: red dotted 1px }
.highlighted .token.code            { color: maroon }
.highlighted .token.code.keyword    { color: navy }
.highlighted .token.typevar         { font-style: italic; }

.highlighted .token.delimiter   {  } /* .[curly,square,parenthesis,angle,array,bracket] */
.highlighted .token.number      {  }    /* .[hex,octal,binary,float] */
.highlighted .token.variable    {  }  /* .[name,value]  */
.highlighted .token.meta        { color: navy }      /* .[content] */

.highlighted .token.bold            { font-weight: bold; }
.highlighted .token.italic          { font-style: italic; }


/* Pretty formatting of code */
.madoko pre.pretty, .madoko code.pretty { 
  font-family: Cambria,Times,Georgia,serif;
  font-size: 100%;
}

.madoko .pretty table {
  border-collapse: collapse;
}
.madoko .pretty td {
  padding: 0em;
}
.madoko .pretty td.empty {
  min-width: 1.5ex;
}
.madoko .pretty td.expander {
  width: 100em;
}
.madoko .pretty .token.identifier         { font-style: italic }
.madoko .pretty .token.constructor        { font-style: italic }


/* ---------------------------------------------------
   Styling for full documents
----------------------------------------------------*/
body.madoko, .madoko-body {
  font-family: Cambria,"Times New Roman","Liberation Serif","Times",serif;
  -webkit-text-size-adjust: 100%; /* so math displays well on mobile devices */
}

body.madoko, .madoko-body, body.madoko.preview[data-view=full] {
  padding: 1em 16% 1em 12%;
}

body.madoko.preview {
  padding: 0em 2em 0em 2em;
}

.madoko p,
.madoko li {
  text-align: justify;
}

/* style h5 and h6 headers a bit better */
.madoko h5, .madoko h6 {
  margin-top: 0.5em;
  margin-bottom: 0pt;
  font-size: 100%;
}
.madoko h5+p {
  margin-top: 0.5em;
}
.madoko h6+p {
  margin-top: 0pt;
}

/* Fix monospace display (see http://code.stephenmorley.org/html-and-css/fixing-browsers-broken-monospace-font-handling/) */
.madoko pre, .madoko code, .madoko kbd, .madoko samp, .madoko tt, .madoko .monospace, .madoko .token.indent, .madoko .reveal pre, .madoko .reveal code, .madoko .email {
  font-family: Consolas,"Andale Mono WT","Andale Mono",Lucida Console,Monaco,monospace,monospace;
  font-size: 0.85em;
}
.madoko pre code, .madoko .token.indent {
  font-size: 0.95em;
}

.madoko pre code {
  font-family: inherit !important;
}

/* Code prettify */
.madoko ol.linenums li {
  background-color: white;
  list-style-type: decimal;
}

/* Merging */
.madoko .remote {
  background-color: #F0FFF0;
}

/* ---------------------------------------------------
   Print settings
----------------------------------------------------*/

@media print {
  body.madoko, .madoko-body {
    font-size: 10pt;
  }
  @page {
    margin: 1in 1.5in;
  }
}

/* ---------------------------------------------------
   Mobile device settings
----------------------------------------------------*/

@media only screen and (max-device-width:1024px) {
  body.madoko, .madoko-body {
    padding-left: 1em;
    padding-right: 1em;
  }
}

  </style>

</head>
<body class="madoko">


<div class="htmlonly"><section class='titleblock align-center'><h1 class='title' data-line='1'>Deconstructing Dynamic Symbolic Execution</h1>


<table><tr><td class='authorblock align-center'><div class='author'>Thomas Ball, Jakub Daniel</div><div class='affiliation address'>Microsoft Research, Charles University</div><div class='email'>tball@microsoft.com, jakub.daniel@d3s.mff.cuni.cz</div></td></tr></table></section></div>
<div class="abstract">
<p data-line="1"><span data-line="1"></span>Dynamic symbolic execution (DSE) is a well-known technique
for automatically generating tests to achieve higher levels
of coverage in a program. Two keys ideas of DSE are
to: (1) seed symbolic execution by executing a program on an
initial input; (2) using concrete values from the program
execution in place of symbolic expressions whenever symbolic
reasoning is hard or not desired. In this paper, we describe
DSE for a simple core language and then present
a minimalist implementation of DSE for Python (in Python) 
that follows this basic recipe. The code is available 
at http://www.github.com/thomasjball/pyexz3/ (tagged <span data-line="11"></span>&#8220;v1.0&#8221;<span data-line="11"></span>) 
and has been designed to make it easy to experiment with and
extend. </p></div><h2 id="sec-intro"   style="bookmark:1.&#8194;Introduction"><span class="heading-before"><span class="heading-label">1</span>.&#8194;</span>Introduction</h2>
<div class="mathdefs hidden input-mathdefs"></div><!-- should we motivate more? -- this dives in deep very quickly -->


<p>Static, path-based symbolic execution explores one control-flow path
at a time through a (sequential) program <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">, using an automated theorem
prover (ATP) to determine if the current path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> is feasible&nbsp;<span class="citations" style="target-element:bibitem">[<a href="#clarke76" title="Lori&#160;A. Clarke. 
A system to generate test data and symbolically execute programs." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">4</span></a>, <a href="#king76" title="James&#160;C. King. 
Symbolic execution and program testing." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">11</span></a>]</span>. 
Ideally, symbolic execution a path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> through program
<img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> yields a logic formula <img src="" alt="$\phi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em"> that describes the set of inputs <img src="" alt="$I$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> (possibly empty)
to program <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> such that for any <img src="" alt="$i \in I$" class="math-inline math" style="vertical-align:-0.042em;height:0.781em">, execution of <img src="" alt="$P(i)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em"> follows path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em">. 
</p>
<p class="indent">If the formula <img src="" alt="$\phi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em"> is unsatisfiable then <img src="" alt="$I$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> is empty and so path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> is not feasible; 
if the formula is satisfiable then <img src="" alt="$I$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> is not empty and so path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> is feasible.
In this case, a model of <img src="" alt="$\phi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em"> provides a witness <img src="" alt="$i \in I$" class="math-inline math" style="vertical-align:-0.042em;height:0.781em">.  Thus, an ATP
that can provide such models can be used in conjunction with
symbolic execution to automatically generate tests to cover paths
in a program. Combined with a search strategy, one gets, in the limit,
an exhaustive white-box testing procedure, for which there are many
applications&nbsp;<span class="citations" style="target-element:bibitem">[<a href="#cadars13" title="Cristian Cadar and Koushik Sen. 
Symbolic execution for software testing: three decades later." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">2</span></a>, <a href="#cadargpde06" title="Cristian Cadar, Vijay Ganesh, Peter&#160;M. Pawlowski, David&#160;L. Dill, and Dawson&#160;R. Engler. 
EXE: automatically generating inputs of death. 
In Proceedings of the 13th ACM Conference on Computer and Communications Security, pages 322&#8211;335, 2006." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">3</span></a>, <a href="#godefroidlm12" title="Patrice Godefroid, Michael&#160;Y. Levin, and David&#160;A. Molnar. 
SAGE: whitebox fuzzing for security testing." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">9</span></a>]</span>. 
</p>
<p class="indent">The formula <img src="" alt="$\phi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em"> is called a <em>path-condition</em> of the path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em">. 
We will see that a given path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> can induce many different path-conditions.
A path-condition <img src="" alt="$\psi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em"> for path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> is <em>sound</em> if 
every input assignment satisfying <img src="" alt="$\psi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em"> defines an
execution of program <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> that follows path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em">&nbsp;<span class="citations" style="target-element:bibitem">[<a href="#godefroid11" title="Patrice Godefroid. 
Higher-order test generation." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">7</span></a>]</span>. 
By its definition, the formula  <img src="" alt="$\phi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em"> is sound and the best representation of <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em">
(as for all sound path-conditions <img src="" alt="$\psi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em">, we have that <img src="" alt="$\psi_p \implies \phi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em">).
In practice, we attempt to compute sound under-approximations of <img src="" alt="$\phi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em"> 
such as <img src="" alt="$\psi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em">. However, we also find it necessary (and useful) to 
compute unsound path-conditions.
</p>
<p class="indent">A path-condition can be translated into the input
language of an ATP, such as&nbsp;<a href="http://z3.codeplex.org/">Z3</a><span class="citations" style="target-element:bibitem">[<a href="#demourab08" title="Leonardo&#160;Mendon&#231;a de&#160;Moura and Nikolaj Bj&#248;rner. 
Z3: an efficient SMT solver." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">5</span></a>]</span>, which provides an answer
of &#8220;unsatisfiable&#8221;, &#8220;satisfiable&#8221; or &#8220;unknown&#8221;, due to theoretical or practical
limitations in automatically deciding satisfiability of various logics.
In the case that the ATP is able to prove &#8220;satisfiable&#8221; we can query it for 
satisfying model in order to generate test inputs. A path-condition 
for <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> can be thought of as function from a
program&#39;s primary inputs to a boolean output representing whether
or not <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> is executed under a given input. Thus, we are asking
the ATP to invert a function when we ask it to decide
the satisfiability/unsatisfiability of a path-condition
</p>
<p class="indent">The static translation of a path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> through a program <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> into 
the most precise path-condition <img src="" alt="$\phi_p$" class="math-inline math" style="vertical-align:-0.304em;height:1.041em"> is not a simple task, as 
programming languages and their semantics are very complex.
Completely characterizing the set of inputs <img src="" alt="$I$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> that follow
path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> means providing a symbolic interpretation of 
every operation in the language so that the
ATP can reason about it. For example, consider a method call in Python. 
Python&#39;s algorithm for method resolution order (see&nbsp;<a href="https://www.python.org/download/releases/2.3/mro/">MRO</a>)
depends on the inheritance hierarchy of the program, a directed, 
acyclic graph that can evolve during program execution. Symbolically
encoding Python&#39;s method resolution order is possible but non-trivial.
There are other reasons it is hard or undesirable to symbolically 
execute various operations, as will detail later.
</p><h3 id="sec-dynamic-symbolic-execution"   style="bookmark:1.1.&#8194;Dynamic symbolic execution"><span class="heading-before"><span class="heading-label">1.1</span>.&#8194;</span>Dynamic symbolic execution</h3>
<p><em>Dynamic</em> symbolic execution (DSE) is a form of path-based
symbolic execution based on two insights. First, the approach 
starts by executing program <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> on
some input <img src="" alt="$i$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">, seeding the symbolic execution process
with a feasible path&nbsp;<span class="citations" style="target-element:bibitem">[<a href="#gupta00" title="Neelam Gupta, Aditya&#160;P. Mathur, and Mary&#160;Lou Soffa. 
Generating test data for branch coverage." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">10</span></a>, <a href="#korel90" title="Bogdan Korel. 
Automated software test data generation." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">12</span></a>, <a href="#korel92" title="Bogdan Korel. 
Dynamic method of software test data generation." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">13</span></a>]</span>. 
Second,  DSE
uses concrete values from the execution <img src="" alt="$P(i)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em"> in place of symbolic expressions 
whenever symbolic reasoning is not possible or desired&nbsp;<span class="citations" style="target-element:bibitem">[<a href="#cadare05" title="Cristian Cadar and Dawson&#160;R. Engler. 
Execution generated test cases: How to make systems code crash itself. 
In Proceedings of 12th International SPIN Workshop, pages 2&#8211;23, 2005." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">1</span></a>, <a href="#godefroidks05" title="Patrice Godefroid, Nils Klarlund, and Koushik Sen. 
DART: directed automated random testing." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">8</span></a>]</span>.
The major benefit of DSE is to
simplify the construction of a symbolic execution tool by
leveraging the concrete execution behavior (given by
actually running the program).
As DSE combines both 
concrete and symbolic reasoning, it also has been called &#8220;concolic&#8221; 
execution&nbsp;<span class="citations" style="target-element:bibitem">[<a href="#senacav06" title="Koushik Sen and Gul Agha. 
CUTE and jcute: Concolic unit testing and explicit path model-checking tools. 
In Proceedings of 18th Computer Aided Verification Conference, pages 419&#8211;423, 2006." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">14</span></a>]</span>.
</p>
<figure id="fig-dse" class="figure align-center"   >
<pre class="para-block pre-fenced pre-fenced3 language-python lang-python python highlighted"  data-line="1" data-line-code="2"><code data-line="2"><span class='token white python'>  </span><span class='token identifier python'>i</span><span class='token white python'> </span><span class='token keyword python'>=</span><span class='token white python'> </span><span class='token identifier python'>an</span><span class='token white python'> </span><span class='token identifier python'>input</span><span class='token white python'> </span><span class='token identifier python'>to</span><span class='token white python'> </span><span class='token identifier python'>program</span><span class='token white python'> </span><span class='token constructor identifier python'>P</span><br><span class='token white python'>  </span><span class='token keyword python'>while</span><span class='token white python'> </span><span class='token identifier python'>defined</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>i</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token keyword python bracket-open'>:</span><br><span class='token white python'>     </span><span class='token identifier python'>p</span><span class='token white python'> </span><span class='token keyword python'>=</span><span class='token white python'> </span><span class='token identifier python'>path</span><span class='token white python'> </span><span class='token identifier python'>covered</span><span class='token white python'> </span><span class='token identifier python'>by</span><span class='token white python'> </span><span class='token identifier python'>execution</span><span class='token white python'> </span><span class='token constructor identifier python'>P</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>i</span><span class='token delimiter parenthesis python bracket-close'>)</span><br><span class='token white python'>     </span><span class='token identifier python'>cond</span><span class='token white python'> </span><span class='token keyword python'>=</span><span class='token white python'> </span><span class='token identifier python'>pathCondition</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>p</span><span class='token delimiter parenthesis python bracket-close'>)</span><br><span class='token white python'>     </span><span class='token identifier python'>s</span><span class='token white python'> </span><span class='token keyword python'>=</span><span class='token white python'> </span><span class='token constructor identifier python'>ATP</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token namespace identifier python'>Not</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>cond</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token delimiter parenthesis python bracket-close'>)</span><br><span class='token white python'>     </span><span class='token identifier python'>i</span><span class='token white python'> </span><span class='token keyword python'>=</span><span class='token white python'> </span><span class='token identifier python'>s</span><span class='token delimiter python'>.</span><span class='token identifier python'>model</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token delimiter parenthesis python bracket-close'>)</span></code></pre>
<hr  class="figureline madoko" data-line="9">

<div data-line="10"><span data-line="10"></span><fig-caption class="figure-caption"><span class="caption-before"><strong>Figure&#160;<span class="figure-label">1</span>.</strong> </span>Pseudo-code for dynamic symbolic execution</fig-caption><span data-line="10"></span>
</div></figure>
<p class="indent">The pseudo-code of Figure&nbsp;<a href="#fig-dse" title="Pseudo-code for dynamic symbolic execution" class="localref" style="target-element:figure"><span class="figure-label">1</span></a> shows the high level process
of DSE. The variable <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>i</span></code> represents an input
to program <code class="code code1 language-python lang-python python highlighted" ><span class='token constructor identifier python'>P</span></code>. Execution of program <code class="code code1 language-python lang-python python highlighted" ><span class='token constructor identifier python'>P</span></code> on the input <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>i</span></code>
traces  a path <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>p</span></code>, from which
a logical formula <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>pathCondition</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>p</span><span class='token delimiter parenthesis python bracket-close'>)</span></code> is constructed.
Finally, the ATP is called with the negation of the path-condition
to find a new input (that hopefully will cover a new path).  This
pseudo-code ellides a number of details that we will deal with later. 
</p>
<figure id="fig-easy-dse" class="figure align-center"   >
<pre class="para-block pre-fenced pre-fenced3 language-python lang-python python highlighted"  data-line="1" data-line-code="2"><code data-line="2"><span class='token keyword python'>def</span><span class='token white python'> </span><span class='token identifier python'>max2</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>s</span><span class='token delimiter python'>,</span><span class='token identifier python'>t</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token keyword python bracket-open'>:</span><br><span class='token white python'>    </span><span class='token keyword python'>if</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>s</span><span class='token white python'> </span><span class='token operator python'>&lt;</span><span class='token white python'> </span><span class='token identifier python'>t</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token keyword python bracket-open'>:</span><br><span class='token white python'>        </span><span class='token keyword python'>return</span><span class='token white python'> </span><span class='token identifier python'>t</span><br><span class='token white python'>    </span><span class='token keyword python'>else</span><span class='token keyword python bracket-open'>:</span><br><span class='token white python'>        </span><span class='token keyword python'>return</span><span class='token white python'> </span><span class='token identifier python'>s</span><br><br><span class='token keyword python'>def</span><span class='token white python'> </span><span class='token identifier python'>max4</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token delimiter python'>,</span><span class='token identifier python'>b</span><span class='token delimiter python'>,</span><span class='token identifier python'>c</span><span class='token delimiter python'>,</span><span class='token identifier python'>d</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token keyword python bracket-open'>:</span><br><span class='token white python'>    </span><span class='token keyword python'>return</span><span class='token white python'> </span><span class='token identifier python'>max2</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>max2</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token delimiter python'>,</span><span class='token identifier python'>b</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token delimiter python'>,</span><span class='token identifier python'>max2</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>c</span><span class='token delimiter python'>,</span><span class='token identifier python'>d</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token delimiter parenthesis python bracket-close'>)</span></code></pre>
<hr  class="figureline madoko" data-line="11">

<div data-line="12"><span data-line="12"></span><fig-caption class="figure-caption"><span class="caption-before"><strong>Figure&#160;<span class="figure-label">2</span>.</strong> </span>Easy example: computing the maximum of four numbers in Python.</fig-caption><span data-line="12"></span>
</div></figure>
<p class="indent para-continue">Consider the  Python function <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>max4</span></code> in Figure&nbsp;<a href="#fig-easy-dse" title="Easy example: computing the maximum of four numbers in Python." class="localref" style="target-element:figure"><span class="figure-label">2</span></a>,
which computes the maximum of four numbers via three calls to
the function <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>max2</span></code>. Suppose we execute <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>max4</span></code> with values
of zero for all four arguments.  In this case, the 
execution path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> contains three comparisons (in the order <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token white python'> </span><span class='token operator python'>&lt;</span><span class='token white python'> </span><span class='token identifier python'>b</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>, 
<code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>c</span><span class='token white python'> </span><span class='token operator python'>&lt;</span><span class='token white python'> </span><span class='token identifier python'>d</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token white python'> </span><span class='token operator python'>&lt;</span><span class='token white python'> </span><span class='token identifier python'>c</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>), all of which evaluate false.
Thus, the path-condition for path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> is <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token keyword python'>not</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token operator python'>&lt;</span><span class='token identifier python'>b</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token keyword python'>not</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>c</span><span class='token operator python'>&lt;</span><span class='token identifier python'>d</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token keyword python'>not</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token white python'> </span><span class='token operator python'>&lt;</span><span class='token white python'> </span><span class='token identifier python'>c</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>.
Negating this condition yields <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token operator python'>&lt;</span><span class='token identifier python'>b</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>or</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>c</span><span class='token operator python'>&lt;</span><span class='token identifier python'>d</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>or</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token operator python'>&lt;</span><span class='token identifier python'>c</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>.
Taking the execution ordering of the three comparisons into account, we
derive three expressions from the negated path-condition to generate
new inputs that will explore execution prefixes of path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> of increasing length:
</p>
<ul class="list-star compact">
<li><em>length 0</em>: <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token operator python'>&lt;</span><span class='token identifier python'>b</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>
</li>
<li><em>length 1</em>: <code class="code code1 language-python lang-python python highlighted" ><span class='token keyword python'>not</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token operator python'>&lt;</span><span class='token identifier python'>b</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>c</span><span class='token operator python'>&lt;</span><span class='token identifier python'>d</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>
</li>
<li><em>length 2</em>: <code class="code code1 language-python lang-python python highlighted" ><span class='token keyword python'>not</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token operator python'>&lt;</span><span class='token identifier python'>b</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token keyword python'>not</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>c</span><span class='token operator python'>&lt;</span><span class='token identifier python'>d</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token operator python'>&lt;</span><span class='token identifier python'>c</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>
</li></ul>

<p>The purpose of taking execution order into account should be clear, as the
comparison <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token operator python'>&lt;</span><span class='token identifier python'>c</span><span class='token delimiter parenthesis python bracket-close'>)</span></code> only executes in the case where <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token keyword python'>not</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token operator python'>&lt;</span><span class='token identifier python'>b</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token keyword python'>not</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>c</span><span class='token operator python'>&lt;</span><span class='token identifier python'>d</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>
holds.
</p><!--

assertions, query

-->


<p class="para-continue">Integer solutions to the above three systems of constraints are:
</p>
<ul class="list-star compact">
<li><code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>a</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>0</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>b</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>2</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>c</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>0</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>d</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>0</span></code>
</li>
<li><code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>a</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>0</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>b</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>0</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>c</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>0</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>d</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>3</span></code>
</li>
<li><code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>a</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>0</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>b</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>0</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>c</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>2</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>d</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>0</span></code>
</li></ul>

<p>In the three cases above, we sought solutions that kept as many of
the variables as possible equal to the original input (in which 
all variables are equal to 0). Execution the <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>max4</span></code> function on the input
corresponding to the first solution produces the path-condition
<code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>a</span><span class='token operator python'>&lt;</span><span class='token identifier python'>b</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token keyword python'>not</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>c</span><span class='token operator python'>&lt;</span><span class='token identifier python'>d</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token keyword python'>not</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>b</span><span class='token white python'> </span><span class='token operator python'>&lt;</span><span class='token white python'> </span><span class='token identifier python'>c</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>, from which we can produce more
inputs.   For this (loop-free function), there are a finite number
of path-conditions. We leave it as an exercise to the reader to 
enumerate them all. 
</p><h3 id="sec-leveraging-concrete-values-in-dse"   style="bookmark:1.2.&#8194;Leveraging concrete values in DSE"><span class="heading-before"><span class="heading-label">1.2</span>.&#8194;</span>Leveraging concrete values in DSE</h3>
<p>We now consider several situations where we can make use of concrete
values in DSE. In the realm of (unbounded-precision) integer arithmetic 
(e.g., bignum integer arithmetic, as in Python 3.0 onwards),
it is easy  to come up with  tiny programs that will be <em>very difficult</em>,
if not <em>impossible</em>, 
for any symbolic execution tool to deal with, such as the function <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>fermat3</span></code>
in Figure&nbsp;<a href="#fig-fermat3" title="Hard example for symbolic execution" class="localref" style="target-element:figure"><span class="figure-label">3</span></a>.  
</p>
<figure id="fig-fermat3" class="figure align-center"   >
<pre class="para-block pre-fenced pre-fenced3 language-python lang-python python highlighted"  data-line="1" data-line-code="2"><code data-line="2"><span class='token keyword python'>def</span><span class='token white python'> </span><span class='token identifier python'>fermat3</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>x</span><span class='token delimiter python'>,</span><span class='token identifier python'>y</span><span class='token delimiter python'>,</span><span class='token identifier python'>z</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token keyword python bracket-open'>:</span><br><span class='token white python'>   </span><span class='token keyword python'>if</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>x</span><span class='token white python'> </span><span class='token operator python'>&gt;</span><span class='token white python'> </span><span class='token number python'>0</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>y</span><span class='token white python'> </span><span class='token operator python'>&gt;</span><span class='token white python'> </span><span class='token number python'>0</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token identifier python'>z</span><span class='token white python'> </span><span class='token operator python'>&gt;</span><span class='token white python'> </span><span class='token number python'>0</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token keyword python bracket-open'>:</span><br><span class='token white python'>      </span><span class='token keyword python'>if</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>x</span><span class='token operator python'>*</span><span class='token identifier python'>x</span><span class='token operator python'>*</span><span class='token identifier python'>x</span><span class='token white python'> </span><span class='token operator python'>+</span><span class='token white python'> </span><span class='token identifier python'>y</span><span class='token operator python'>*</span><span class='token identifier python'>y</span><span class='token operator python'>*</span><span class='token identifier python'>y</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token identifier python'>z</span><span class='token operator python'>*</span><span class='token identifier python'>z</span><span class='token operator python'>*</span><span class='token identifier python'>z</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token keyword python bracket-open'>:</span><br><span class='token white python'>          </span><span class='token keyword python'>return</span><span class='token white python'> </span><span class='token string delim python bracket-open'>&quot;</span><span class='token string python'>Fermat and Wiles were wrong!?!</span><span class='token string delim python bracket-close'>&quot;</span><br><span class='token white python'>   </span><span class='token keyword python'>return</span><span class='token white python'> </span><span class='token number python'>0</span></code></pre>
<hr  class="figureline madoko" data-line="8">

<div data-line="9"><span data-line="9"></span><fig-caption class="figure-caption"><span class="caption-before"><strong>Figure&#160;<span class="figure-label">3</span>.</strong> </span>Hard example for symbolic execution</fig-caption><span data-line="9"></span>
</div></figure>
<p class="indent">Fermat&#39;s Last Theorem, proved
by Andrew Wiles in the late 20th century, states that no 
three positive integers <img src="" alt="$x$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">, <img src="" alt="$y$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em">, and <img src="" alt="$z$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> can satisfy the equation
<img src="" alt="$x^n + y^n = z^n$" class="math-inline math" style="vertical-align:-0.212em;height:0.937em"> for any integer value of <img src="" alt="$n$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> greater than two.
The function <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>fermat3</span></code> encodes this statement for <img src="" alt="$n=3$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em">.   It
is not reasonable to have a computer waste time trying to find
a solution that would cause <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>fermat3</span></code> to print the string 
<code class="code code1 language-python lang-python python highlighted" ><span class='token string delim python bracket-open'>&quot;</span><span class='token string python'>Fermat and Wiles were wrong!?!</span><span class='token string delim python bracket-close'>&quot;</span></code>.  In cases of complex (non-linear)
arithmetic operations,
such as <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>x</span><span class='token operator python'>*</span><span class='token identifier python'>x</span><span class='token operator python'>*</span><span class='token identifier python'>x</span></code>, we might choose to treat the operation concretely.
</p>
<p class="indent">There are a number of ways to deal with the above issue: one is 
to recognize all non-linear terms in a symbolic expression and replace
them with their concrete counterparts during execution. For the <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>fermat3</span></code> 
example, this would mean that during DSE the symbolic expression 
<code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>x</span><span class='token operator python'>*</span><span class='token identifier python'>x</span><span class='token operator python'>*</span><span class='token identifier python'>x</span><span class='token white python'> </span><span class='token operator python'>+</span><span class='token white python'> </span><span class='token identifier python'>y</span><span class='token operator python'>*</span><span class='token identifier python'>y</span><span class='token operator python'>*</span><span class='token identifier python'>y</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token identifier python'>z</span><span class='token operator python'>*</span><span class='token identifier python'>z</span><span class='token operator python'>*</span><span class='token identifier python'>z</span><span class='token delimiter parenthesis python bracket-close'>)</span></code> would be reduced to the constant <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>False</span></code>
by evaluation on the concrete values of variables <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>x</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>y</span></code> and <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>z</span></code>.
</p>
<p class="indent">Besides difficult operations (such as non-linear arithmetic),
other examples of code that we might treat
concretely instead of symbolically include
functions that are hard to invert, such as cryptographic hash functions,
or low-level functions that we do not wish to test (such as 
operating system functions).  Consider
the code in Figure&nbsp;<a href="#fig-hash" title="Another hard example for symbolic execution" class="localref" style="target-element:figure"><span class="figure-label">4</span></a>, which applies the function
<code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>unknown</span></code> to argument <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>x</span></code> and compares it to argument <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>y</span></code>.
By using the name <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>unknown</span></code> we simply mean to say that we 
wish treat this function as a black box, with no knowledge
of how it operates internally. 
</p>
<figure id="fig-hash" class="figure align-center"   >
<pre class="para-block pre-fenced pre-fenced3 language-python lang-python python highlighted"  data-line="1" data-line-code="2"><code data-line="2"><span class='token keyword python'>def</span><span class='token white python'> </span><span class='token identifier python'>dart</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>x</span><span class='token delimiter python'>,</span><span class='token identifier python'>y</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token keyword python bracket-open'>:</span><br><span class='token white python'>  </span><span class='token keyword python'>if</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>unknown</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>x</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token identifier python'>y</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token keyword python bracket-open'>:</span><br><span class='token white python'>     </span><span class='token keyword python'>return</span><span class='token white python'> </span><span class='token number python'>1</span><br><span class='token white python'>  </span><span class='token keyword python'>return</span><span class='token white python'> </span><span class='token number python'>0</span></code></pre>
<hr  class="figureline madoko" data-line="7">

<div data-line="8"><span data-line="8"></span><fig-caption class="figure-caption"><span class="caption-before"><strong>Figure&#160;<span class="figure-label">4</span>.</strong> </span>Another hard example for symbolic execution</fig-caption><span data-line="8"></span>
</div></figure>
<p class="indent">In such a case, we can use DSE to execute the function <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>unknown</span></code>
function on a specific input (say <code class="code code1 language-python lang-python python highlighted" ><span class='token number python'>5013</span></code>) and observe its output
(say 42). That is, rather than try to execute <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>unknown</span></code> symbolically
and invoke an ATP to invert the function&#39;s path-condition, we
simply treat the call to <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>unknown</span></code> concretely, substituting
its return value (in this case <code class="code code1 language-python lang-python python highlighted" ><span class='token number python'>42</span></code>) for the specialized expression 
<code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>unknown</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token number python'>5013</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token identifier python'>y</span></code> to get the predicate <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token number python'>42</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token identifier python'>y</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>. 
</p>
<p class="indent">Adding the constraint <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>x</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>5013</span><span class='token delimiter parenthesis python bracket-close'>)</span></code> yields the sound but
rather specific path-condition 
<code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>x</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token number python'>5013</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token keyword python'>and</span><span class='token white python'> </span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token number python'>42</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token identifier python'>y</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>.
Note that the path-condition <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token number python'>42</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token identifier python'>y</span><span class='token delimiter parenthesis python bracket-close'>)</span></code> is not sound, as it admits
any value for the variable <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>x</span></code>, which likely includes many values
for which <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>unknown</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>x</span><span class='token delimiter parenthesis python bracket-close'>)</span><span class='token white python'> </span><span class='token operator python'>==</span><span class='token white python'> </span><span class='token identifier python'>y</span><span class='token delimiter parenthesis python bracket-close'>)</span></code> is false.
</p><h3 id="sec-overview"   style="bookmark:1.3.&#8194;Overview"><span class="heading-before"><span class="heading-label">1.3</span>.&#8194;</span>Overview</h3>
<p class="para-continue">This introduction elides many important 
issues that arise in implementing DSE for a real language, which we will 
focus on in the remainder of the paper. These include how to:
</p>
<ul class="list-star compact">
<li>Identify the code under test <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> and the symbolic inputs to <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">;
</li>
<li>Trace the control flow path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> taken by execution <img src="" alt="$P(i)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">;
</li>
<li>Reinterpret program operations to compute symbolic expressions;
</li>
<li>Generate a path-condition from <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> and the symbolic expressions;
</li>
<li>Generate a new input <img src="" alt="$i&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> by negating (part of) the path-condition, translating
the path-condition to the input language of an ATP, invoking the ATP, and
lifting a satisfying model (if any) back up to the source level;
</li>
<li>Guide the search to expose new paths.
</li></ul>

<p>The rest of this paper is organized as follows. Section&nbsp;<a href="#sec-semantics" title="2.&#8194;Instrumented Types" class="localref" style="target-element:h1"><span class="heading-label">2</span></a> 
describes an instrumented typing discipline where we lift each type (representing 
a set of concrete values) to a symbolic type (representing
a set of pairs of concrete and symbolic values).
Section&nbsp;<a href="#sec-sp2dse" title="3.&#8194;From Strongest Postconditions to DSE" class="localref" style="target-element:h1"><span class="heading-label">3</span></a> shows how strongest postconditions defines a symbolic
semantics for a small programming language and how strongest postconditions
can be refined to model DSE.
Section&nbsp;<a href="#sec-impl" title="4.&#8194;Architecture of PyExZ3" class="localref" style="target-element:h1"><span class="heading-label">4</span></a> describes an implementation of DSE for the Python language
in the Python language that follows the instrumented semantics pattern closely
(full implementation and tests available at&nbsp;<a href="http://www.github.com/thomasjball/pyexz3">PyExZ3</a>, tagged &#8220;v1.0&#8221;).
Section&nbsp;<a href="#sec-int2z3" title="5.&#8194;From Python Integers to Z3 Arithmetic" class="localref" style="target-element:h1"><span class="heading-label">5</span></a> describes the symbolic encoding of Python integer 
operations using two decision procedures of Z3: linear arithmetic with
uninterpreted functions in place of non-linear operations;
fixed-width bitvectors with precise encodings of most operations.
Section&nbsp;<a href="#sec-extensions" title="6.&#8194;Extensions" class="localref" style="target-element:h1"><span class="heading-label">6</span></a> offers a number of ideas for projects
to extend the capabilities of&nbsp;<a href="http://www.github.com/thomasjball/pyexz3">PyExZ3</a>.
</p><h2 id="sec-semantics"   style="bookmark:2.&#8194;Instrumented Types"><span class="heading-before"><span class="heading-label">2</span>.&#8194;</span>Instrumented Types</h2>
<p>We are given a universe of classes/types <img src="" alt="$U$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">; a type <img src="" alt="$T \in U$" class="math-inline math" style="vertical-align:-0.044em;height:0.807em"> carries
along a  set of operations that apply to values of type <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em">,
where an operation <img src="" alt="$o \in T$" class="math-inline math" style="vertical-align:-0.044em;height:0.807em">  takes an argument list of typed 
values as input (the first being of type <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em">) and produces a single 
typed value as output. Nullary (static) operations of type <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> can be 
used to create values of type <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> (such as constants, objects, etc.)
</p>
<p class="indent para-continue">A program <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> has typed input variables
<img src="" alt="$v_1 : T_1 \ldots v_k : T_k$" class="math-inline math" style="vertical-align:-0.164em;height:0.911em"> and a body from the language of statements <img src="" alt="$S$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">:
</p>
<div class="mathpre para-block input-mathpre"><img src="" alt="\[\begin{mdMathprearray}%
\mathid{S}\mdMathspace{1}\rightarrow   &amp;\mdMathspace{1}\mathid{v}\mdMathspace{1}:=\mdMathspace{1}\mathid{E}\mdMathbr{}
\mdMathindent{3}|\mdMathspace{1}&amp;\mdMathspace{1}\mathkw{skip}\mdMathspace{1}\mdMathbr{}
\mdMathindent{3}|\mdMathspace{1}&amp;\mdMathspace{1}\mathid{S}_1\mdMathspace{1};\mdMathspace{1}\mathid{S}_2\mdMathspace{1}\mdMathbr{}
\mdMathindent{3}|\mdMathspace{1}&amp;\mdMathspace{1}\mathkw{if}\mdMathspace{1}\mathid{E}\mdMathspace{1}\mathkw{then}\mdMathspace{1}\mathid{S}_1\mdMathspace{1}\mathkw{else}\mdMathspace{1}\mathid{S}_2\mdMathspace{1}\mathkw{end}\mdMathbr{}
\mdMathindent{3}|\mdMathspace{1}&amp;\mdMathspace{1}\mathkw{while}\mdMathspace{1}\mathid{E}\mdMathspace{1}\mathkw{do}\mdMathspace{1}\mathid{S}\mdMathspace{1}\mathkw{end}
\end{mdMathprearray}\]" class="math-display math" style="vertical-align:-0.000em;height:6.218em"></div>
<p>The language of expressions (<img src="" alt="$E$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em">) is defined by the application of operations
to values, where constants (nullary operations) and 
program variables form the leaves 
of the expression tree and non-nullary operators 
form the interior nodes of the tree.
For now, we will consider all values to be immutable.
That is, the only source of mutation in the language is the 
assignment statement.
</p>
<p class="indent para-continue">To introduce symbolic execution into the picture,
we can imagine that a type <img src="" alt="$T \in U$" class="math-inline math" style="vertical-align:-0.044em;height:0.807em"> has
(one or more) counterparts in a symbolic universe <img src="" alt="$U&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em">. A type <img src="" alt="$T&#39; \in U&#39;$" class="math-inline math" style="vertical-align:-0.044em;height:0.885em">
is a subtype of <img src="" alt="$T \in U$" class="math-inline math" style="vertical-align:-0.044em;height:0.807em"> with two purposes:
</p>
<ul class="list-star loose">
<li>
<p>First, a value of type <img src="" alt="$T&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> represents a pair of values: 
a concrete value <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> of (super)type <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> and a symbolic expression <img src="" alt="$e$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">. 
A symbolic expression is a tree
whose leaves are either nullary operators (i.e., constants) of a type in <img src="" alt="$U$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">
or are Skolem constants representing the (symbolic) inputs (<img src="" alt="$v_1 \ldots v_k$" class="math-inline math" style="vertical-align:-0.161em;height:0.624em">)
to the program <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">, and whose interior nodes represent operations 
from types in <img src="" alt="$U$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">. We refer to Skolem constants as &#8220;symbolic constants&#8221;
from this point on. Note that symbolic expressions do not contain
references to program variables.
</p></li>
<li>
<p>Second, the type <img src="" alt="$T&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> redefines some of the operations <img src="" alt="$o \in T$" class="math-inline math" style="vertical-align:-0.044em;height:0.807em">,
namely those for which we wish to compute symbolic expressions.
An operation <img src="" alt="$o \in T&#39;$" class="math-inline math" style="vertical-align:-0.044em;height:0.885em"> has the same parameter list as <img src="" alt="$o \in T$" class="math-inline math" style="vertical-align:-0.044em;height:0.807em">, allowing it
to take inputs with types from both <img src="" alt="$U$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> and <img src="" alt="$U&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em">. The return type
of <img src="" alt="$o \in T&#39;$" class="math-inline math" style="vertical-align:-0.044em;height:0.885em"> generally is from <img src="" alt="$U&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> (though it can be from <img src="" alt="$U$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">). 
Thus, <img src="" alt="$o \in T&#39;$" class="math-inline math" style="vertical-align:-0.044em;height:0.885em"> is a proper function subtype of <img src="" alt="$o \in T$" class="math-inline math" style="vertical-align:-0.044em;height:0.807em">. 
The purpose of <img src="" alt="$o \in T&#39;$" class="math-inline math" style="vertical-align:-0.044em;height:0.885em"> is to:
(1) perform operation <img src="" alt="$o \in T$" class="math-inline math" style="vertical-align:-0.044em;height:0.807em"> on the concrete 
values associated with its inputs; 
(2) build a symbolic expression tree rooted at operation <img src="" alt="$o$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> 
whose children are the trees associated with the inputs to <img src="" alt="$o$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">. 
</p></li></ul>

<p>Figure&nbsp;<a href="#fig-subtype" title="Type instrumentation to carry both concrete values and symbolic expressions." class="localref" style="target-element:figure"><span class="figure-label">5</span></a> presents pseudo code for the instrumention
of a type <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> via a type <img src="" alt="$T&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em">.
The class <code class="code code2 language-cpp2 lang-cpp2 cpp2 highlighted" ><span class='token type identifier cpp2'>Symbolic</span></code> is used to hold an expression tree (<code class="code code2 language-cpp2 lang-cpp2 cpp2 highlighted" ><span class='token type identifier cpp2'>Expr</span></code>).
Given a class <img src="" alt="$T \in U$" class="math-inline math" style="vertical-align:-0.044em;height:0.807em">, a symbolic type <img src="" alt="$T&#39; \in U&#39;$" class="math-inline math" style="vertical-align:-0.044em;height:0.885em"> is defined by inheriting 
from both <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> and <code class="code code2 language-cpp2 lang-cpp2 cpp2 highlighted" ><span class='token type identifier cpp2'>Symbolic</span></code>. This ensures that a <img src="" alt="$T&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> can be used
whereever a <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> is expected. 
</p>
<figure id="fig-subtype" class="figure align-center"   >
<pre class="para-block pre-fenced pre-fenced3 language-cpp2 lang-cpp2 cpp2 highlighted" data-line="1" data-line-code="2" ><code data-line="2"><span class='token white cpp2'>  </span><span class='token keyword cpp2'>class</span><span class='token white cpp2'> </span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$T&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"></span></span><span class='token white cpp2'> </span><span class='token operator cpp2'>:</span><span class='token white cpp2'> </span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"></span></span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token type identifier cpp2'>Symbolic</span><span class='token white cpp2'> </span><span class='token delimiter curly cpp2 bracket-open'>{</span><br><span class='token white cpp2'>    </span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$T&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"></span></span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token identifier cpp2'>c</span><span class='token operator cpp2'>:</span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"></span></span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>e</span><span class='token operator cpp2'>:</span><span class='token type identifier cpp2'>Expr</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><span class='token white cpp2'> </span><span class='token operator cpp2'>:</span><span class='token white cpp2'> </span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"></span></span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token identifier cpp2'>c</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token source cpp2'>S</span><span class='token identifier cpp2'>ymbolic</span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token identifier cpp2'>e</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><span class='token white cpp2'> </span><span class='token delimiter curly cpp2 bracket-open'>{</span><span class='token delimiter curly cpp2 bracket-close'>}</span><br><br><span class='token white cpp2'>    </span><span class='token keyword extra cpp2'>override</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>o</span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token keyword cpp2'>this</span><span class='token operator cpp2'>:</span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"></span></span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>f1</span><span class='token operator cpp2'>:</span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$T_1$" class="math-inline math" style="vertical-align:-0.164em;height:0.911em"></span></span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>.</span><span class='token white cpp2'> </span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>fk</span><span class='token operator cpp2'>:</span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$T_k$" class="math-inline math" style="vertical-align:-0.164em;height:0.911em"></span></span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><span class='token white cpp2'> </span><span class='token operator cpp2'>:</span><span class='token white cpp2'> </span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$R&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"></span></span><span class='token white cpp2'> </span><span class='token delimiter curly cpp2 bracket-open'>{</span><br><span class='token white cpp2'>      </span><span class='token keyword extra cpp2'>var</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>c</span><span class='token white cpp2'> </span>:=<span class='token white cpp2'> </span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"></span></span><span class='token delimiter cpp2'>.</span><span class='token identifier cpp2'>o</span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token keyword cpp2'>this</span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>f1</span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>.</span><span class='token white cpp2'> </span><span class='token delimiter cpp2'>,</span><span class='token identifier cpp2'>fk</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><br><span class='token white cpp2'>      </span><span class='token keyword extra cpp2'>var</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>e</span><span class='token white cpp2'> </span>:=<span class='token white cpp2'> </span><span class='token keyword cpp2'>new</span><span class='token white cpp2'> </span><span class='token source cpp2'>E</span><span class='token identifier cpp2'>xpr</span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"></span></span><span class='token delimiter cpp2'>.</span><span class='token identifier cpp2'>o</span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>expr</span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token identifier cpp2'>self</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>expr</span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token identifier cpp2'>f1</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>expr</span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token identifier cpp2'>fk</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><br><span class='token white cpp2'>      </span><span class='token keyword cpp2'>return</span><span class='token white cpp2'> </span><span class='token keyword cpp2'>new</span><span class='token white cpp2'> </span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$R&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"></span></span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token identifier cpp2'>c</span><span class='token delimiter cpp2'>,</span><span class='token identifier cpp2'>e</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><span class='token white cpp2'> </span><br><span class='token white cpp2'>    </span><span class='token delimiter curly cpp2 bracket-close'>}</span><br><span class='token white cpp2'>    </span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>.</span><br><span class='token white cpp2'>  </span><span class='token delimiter curly cpp2 bracket-close'>}</span><br><span class='token white cpp2'>  </span><br><span class='token white cpp2'>  </span><span class='token keyword cpp2'>class</span><span class='token white cpp2'> </span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$R&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"></span></span><span class='token white cpp2'> </span><span class='token operator cpp2'>:</span><span class='token white cpp2'> </span><span class='token type identifier cpp2'><span class="code-escaped"><img src="" alt="$R$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"></span></span><span class='token delimiter cpp2'>,</span><span class='token white cpp2'> </span><span class='token type identifier cpp2'>Symbolic</span><span class='token white cpp2'> </span><span class='token delimiter curly cpp2 bracket-open'>{</span><span class='token white cpp2'> </span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>.</span><span class='token delimiter cpp2'>.</span><span class='token white cpp2'> </span><span class='token delimiter curly cpp2 bracket-close'>}</span><br><span class='token white cpp2'>  </span><br><span class='token white cpp2'>  </span><span class='token keyword extra cpp2'>function</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>expr</span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token identifier cpp2'>v</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><span class='token white cpp2'> </span><span class='token operator cpp2'>=</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>v</span><span class='token white cpp2'> </span><span class='token keyword extra cpp2'>instanceof</span><span class='token white cpp2'> </span><span class='token type identifier cpp2'>Symbolic</span><span class='token white cpp2'> </span><span class='token operator cpp2'>?</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>v</span><span class='token delimiter cpp2'>.</span><span class='token identifier cpp2'>getExpr</span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span><span class='token white cpp2'> </span><span class='token operator cpp2'>:</span><span class='token white cpp2'> </span><span class='token identifier cpp2'>v</span></code></pre>
<hr  class="figureline madoko" data-line="17">

<div data-line="18"><span data-line="18"></span><fig-caption class="figure-caption"><span class="caption-before"><strong>Figure&#160;<span class="figure-label">5</span>.</strong> </span>Type instrumentation to carry both concrete values and symbolic expressions.</fig-caption><span data-line="18"></span>
</div></figure>
<p class="indent para-continue">A type such as <img src="" alt="$T&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em">  only can be constructed by providing a concrete value <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> of 
type <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> and a symbolic expression <img src="" alt="$e$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> to the constructor for <img src="" alt="$T&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em">.
This will be done in exactly two places:
</p>
<ul class="list-star loose">
<li>
<p>by the creation of symbolic constants associated with the primary
inputs (<img src="" alt="$v_1 \ldots v_k$" class="math-inline math" style="vertical-align:-0.161em;height:0.624em">) to the program;
</p></li>
<li>
<p>by the instrumented operations as shown  in Figure&nbsp;<a href="#fig-subtype" title="Type instrumentation to carry both concrete values and symbolic expressions." class="localref" style="target-element:figure"><span class="figure-label">5</span></a>. 
</p></li></ul>

<p>An instrumented operation <img src="" alt="$o$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> on arguments (<code class="code code2 language-cpp2 lang-cpp2 cpp2 highlighted" ><span class='token keyword cpp2'>this</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>f1</span></code>, &#8230;, <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>fk</span></code>)
first invokes its corresponding underlying
operator <img src="" alt="$T.o$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> on arguments (<code class="code code2 language-cpp2 lang-cpp2 cpp2 highlighted" ><span class='token keyword cpp2'>this</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>f1</span></code>, &#8230;, <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>fk</span></code>) to get concrete value <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>c</span></code>.
It then constructs a new expression tree <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>e</span></code>
rooted at operator <img src="" alt="$T.o$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em">, whose children are the result of
mapping the function <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>expr</span></code> over (<code class="code code2 language-cpp2 lang-cpp2 cpp2 highlighted" ><span class='token keyword cpp2'>this</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>f1</span></code>, &#8230;, <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>fk</span></code>). 
The helper function <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>expr</span><span class='token delimiter parenthesis python bracket-open'>(</span><span class='token identifier python'>v</span><span class='token delimiter parenthesis python bracket-close'>)</span></code>
evaluates to an expression tree in the case that <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>v</span></code> is of <code class="code code2 language-cpp2 lang-cpp2 cpp2 highlighted" ><span class='token type identifier cpp2'>Symbolic</span></code> type
(representing a type in <img src="" alt="$U&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em">) and evaluates to <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>v</span></code> itself, a concrete value
of some type in <img src="" alt="$U$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">, otherwise.
Finally, having computed the values <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>c</span></code> and <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>e</span></code>, the instrumented operator 
returns <code class="code code2 language-cpp2 lang-cpp2 cpp2 highlighted" ><span class="code-escaped"><img src="" alt="$R&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"></span><span class='token delimiter parenthesis cpp2 bracket-open'>(</span><span class='token identifier cpp2'>c</span><span class='token delimiter cpp2'>,</span><span class='token identifier cpp2'>e</span><span class='token delimiter parenthesis cpp2 bracket-close'>)</span></code>, where <img src="" alt="$R$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> is the return type of operator <img src="" alt="$T.o$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em">,
and <img src="" alt="$R&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> is a subtype of <img src="" alt="$R$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> from universe <img src="" alt="$U&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em">.
</p>
<p class="indent">Looked at another way, the universe <img src="" alt="$U&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> represents the &#8220;tainting&#8221; of
types from <img src="" alt="$U$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">. Tainted values flow from program inputs to the 
operands of operators. If an operator has been redefined
(as above) then taintedness propagates from its inputs to its outputs.
On the other hand, if the operator has not been redefined, then it will
not propagate taintedness. In the context of DSE, &#8220;taintedness&#8221; means
that the instrumented semantics carries along a symbolic expression tree <img src="" alt="$e$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">
along with a concrete value <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">.
</p>
<p class="indent">The choice of types from the universe <img src="" alt="$U&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> determines how symbolic
expressions are constructed. For each <img src="" alt="$T \in U$" class="math-inline math" style="vertical-align:-0.044em;height:0.807em">, the &#8220;most symbolic&#8221;
(least concrete) choice is the <img src="" alt="$T&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> that redefines every operator of <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em">
(as shown in Figure&nbsp;<a href="#fig-subtype" title="Type instrumentation to carry both concrete values and symbolic expressions." class="localref" style="target-element:figure"><span class="figure-label">5</span></a>).
The &#8220;least symbolic&#8221; (most concrete) choice is <img src="" alt="$T&#39; = T$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> which
redefines no operators.  Let <img src="" alt="$symbolic(T)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em"> be the
set of types in <img src="" alt="$U&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> that are subtypes of <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em">. The types
in <img src="" alt="$symbolic(T)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em"> are partially ordered by subset inclusion on the 
set of operators from <img src="" alt="$T$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> they redefine.
</p><!-- Example of an instrumentation -->

<h2 id="sec-sp2dse"   style="bookmark:3.&#8194;From Strongest Postconditions to DSE"><span class="heading-before"><span class="heading-label">3</span>.&#8194;</span>From Strongest Postconditions to DSE</h2>
<p>The previous section showed how symbolic expressions can be computed via a
set of instrumented types, where the expressions are computed as a side-effect 
of the execution of program operations.
This section shows how these symbolic expressions can be used to form a 
<em>path-condition</em> (which then can be compiled into a logic formula and 
passed to an automated theorem prover to find new inputs to drive a 
program&#39;s execution along new paths). We derive a <em>path-condition</em>
directly from the <em>strongest postcondition</em> (symbolic) semantics of our
programming language, refining it to model the basic operations
of an interpreter. 
</p><h3 id="sec-strongest-postconditions"   style="bookmark:3.1.&#8194;Strongest Postconditions"><span class="heading-before"><span class="heading-label">3.1</span>.&#8194;</span>Strongest Postconditions</h3>
<p class="para-continue">The strongest postcondition transformer <img src="" alt="$SP$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">&nbsp;<span class="citations" style="target-element:bibitem">[<a href="#dijkstra76" title="Edsger&#160;W. Dijkstra. 
A Discipline of Programming." class="bibref localref" style="target-element:bibitem"><span class="bibitem-label">6</span></a>]</span> is defined over
a predicate <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> representing a set of 
pre-states and a statement <img src="" alt="$S$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> from our language. The transformer <img src="" alt="$Q = SP(P,S)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">
yields a predicate <img src="" alt="$Q$" class="math-inline math" style="vertical-align:-0.207em;height:0.937em"> such that for any state <img src="" alt="$s$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> satisfying
predicate <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">, the execution of statement <img src="" alt="$S$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> from state <img src="" alt="$s$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">,
if it does not go wrong or diverge, yields a state <img src="" alt="$s&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> satisfying predicate <img src="" alt="$Q$" class="math-inline math" style="vertical-align:-0.207em;height:0.937em">. 
The strongest postcondition for the statements in our language
is defined by the following five rules:
</p>
<div class="mathpre para-block input-mathpre"><img src="" alt="\[\begin{mdMathprearray}%
1.\mdMathspace{2}&amp;\mdMathspace{1}\mathid{SP}(\mathid{P},\mdMathspace{1}\mathid{x}\mdMathspace{1}:=\mdMathspace{1}\mathid{E})\mdMathspace{1}{~\buildrel\triangle\over=~}\mdMathspace{1}\exists \mathid{y}\mdMathspace{1}.\mdMathspace{1}(\mathid{x}\mdMathspace{1}=\mdMathspace{1}\mathid{E}\mdMathspace{1}[\mdMathspace{1}\mathid{x}\mdMathspace{1}\rightarrow \mathid{y}\mdMathspace{1}])\mdMathspace{1}\wedge \mathid{P}\mdMathspace{1}[\mdMathspace{1}\mathid{x}\mdMathspace{1}\rightarrow \mathid{y}\mdMathspace{1}]\mdMathbr{}
2.\mdMathspace{2}&amp;\mdMathspace{1}\mathid{SP}(\mathid{P},\mdMathspace{1}\mathkw{skip})\mdMathspace{1}{~\buildrel\triangle\over=~}\mdMathspace{1}\mathid{P}\mdMathbr{}
3.\mdMathspace{2}&amp;\mdMathspace{1}\mathid{SP}(\mathid{P},\mathid{S}_{1};\mathid{S}_{2})\mdMathspace{1}{~\buildrel\triangle\over=~}\mdMathspace{1}\mathid{SP}(\mathid{SP}(\mathid{P},\mathid{S}_{1}),\mdMathspace{1}\mathid{S}_{2})\mdMathbr{}
4.\mdMathspace{2}&amp;\mdMathspace{1}\mathid{SP}(\mathid{P},\mathkw{if}\mdMathspace{1}\mathid{E}\mdMathspace{1}\mathkw{then}\mdMathspace{1}\mathid{S}_1\mdMathspace{1}\mathkw{else}\mdMathspace{1}\mathid{S}_2\mdMathspace{1}\mathkw{end})\mdMathspace{1}{~\buildrel\triangle\over=~}\mdMathbr{}
\mdMathindent{4}&amp;\mdMathspace{7}\mathid{SP}(\mathid{P}\wedge \mathid{E},\mathid{S}_1)\mdMathspace{1}\vee  \mathid{SP}(\mathid{P}\mdMathspace{1}\wedge \neg \mathid{E},\mathid{S}_2)\mdMathbr{}
5.\mdMathspace{2}&amp;\mdMathspace{1}\mathid{SP}(\mathid{P},\mathkw{while}\mdMathspace{1}\mathid{E}\mdMathspace{1}\mathkw{do}\mdMathspace{1}\mathid{S}\mdMathspace{1}\mathkw{end})\mdMathspace{1}{~\buildrel\triangle\over=~}\mdMathbr{}
\mdMathindent{4}&amp;\mdMathspace{6}\mathid{SP}(\mathid{P},\mathkw{if}\mdMathspace{1}\mathid{E}\mdMathspace{1}\mathkw{then}\mdMathspace{1}\mathid{S};\mdMathspace{1}\mathkw{while}\mdMathspace{1}\mathid{E}\mdMathspace{1}\mathkw{do}\mdMathspace{1}\mathid{S}\mdMathspace{1}\mathkw{end}\mdMathspace{1}\mathkw{else}\mdMathspace{1}\mathkw{skip}\mdMathspace{1}\mathkw{end})
\end{mdMathprearray}\]" class="math-display math" style="vertical-align:-0.000em;height:10.849em"></div>
<p>Rule (1) defines the strongest postcondition for 
the assignment statement. The assignment is modelled
logically by the equality <img src="" alt="$x = E$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> where any free occurrence of <img src="" alt="$x$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> in <img src="" alt="$E$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em">
is replaced by the existentially quantified variable <img src="" alt="$y$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em">, which represents
the value of <img src="" alt="$x$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> in the pre-state. The same substitution (<img src="" alt="$[x \rightarrow y ]$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">)
is applied to the pre-state predicate <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">. 
</p>
<p class="indent">Rules (2)-(5) define the strongest postcondition for the four control-flow
statements. The rules for the <strong>skip</strong> statement and sequencing (;) are
straightforward. 
Of particular interest, note that the rule for the <strong>if-then-else</strong> 
statement splits cases on the expression <img src="" alt="$E$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em">. 
It is here that DSE will choose one of the cases for us, as the concrete
execution will evaluate <img src="" alt="$E$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> either to be true or false. This gives rise
to the path-condition (either <img src="" alt="$P \wedge E$" class="math-inline math" style="vertical-align:-0.000em;height:0.781em"> or <img src="" alt="$P \wedge \neg E$" class="math-inline math" style="vertical-align:-0.000em;height:0.781em">). The
recursive rule for the <strong>while</strong> loop unfolds as many times as the
expression <img src="" alt="$E$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> evaluates true, adding to the path-condition.
</p><h3 id="sp-refined"   style="bookmark:3.2.&#8194;From $SP$ to DSE"><span class="heading-before"><span class="heading-label">3.2</span>.&#8194;</span>From <img src="" alt="$SP$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> to DSE</h3>
<p>Assume that an execution begins with the assignment of initial values <img src="" alt="$c_1 \ldots c_k$" class="math-inline math" style="vertical-align:-0.161em;height:0.624em"> to the program <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">&#39;s inputs
<img src="" alt="$V = \{ v_1 : T_1 \ldots v_k : T_k \}$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">.  To seed symbolic execution, some of the types <img src="" alt="$T_i$" class="math-inline math" style="vertical-align:-0.164em;height:0.911em"> are
replaced by symbolic counterparts <img src="" alt="$T&#39;_i$" class="math-inline math" style="vertical-align:-0.281em;height:1.093em">, in which case
<img src="" alt="$v_i$" class="math-inline math" style="vertical-align:-0.161em;height:0.624em"> is initialized to the value <img src="" alt="$sc_i = T&#39;_i (c_i,SC(v_i))$" class="math-inline math" style="vertical-align:-0.288em;height:1.119em"> instead of the value <img src="" alt="$c_i$" class="math-inline math" style="vertical-align:-0.161em;height:0.624em">,
where <img src="" alt="$SC(v_i)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em"> is the symbolic constant representing the initial value of variable <img src="" alt="$v_i$" class="math-inline math" style="vertical-align:-0.161em;height:0.624em">.
The symbolic constant <img src="" alt="$SC(v_i)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em"> can be thought of as representing any value of
type <img src="" alt="$T_i$" class="math-inline math" style="vertical-align:-0.164em;height:0.911em">, which includes the value <img src="" alt="$c_i$" class="math-inline math" style="vertical-align:-0.161em;height:0.624em">.  
</p>
<p class="indent para-continue">Let <img src="" alt="$V_s$" class="math-inline math" style="vertical-align:-0.159em;height:0.885em"> and <img src="" alt="$V_c$" class="math-inline math" style="vertical-align:-0.159em;height:0.885em"> partition the variables of <img src="" alt="$V$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> into those variables
that are treated symbolically (<img src="" alt="$V_s$" class="math-inline math" style="vertical-align:-0.159em;height:0.885em">) and those that are treated concretely 
(<img src="" alt="$V_c$" class="math-inline math" style="vertical-align:-0.159em;height:0.885em">). The initial state of the program is characterized by the formula
</p>
<div class="equation align-center para-block" style="line-adjust:0"><span class="equation-before"><span class="equation-label">(1)</span></span>

<div class="math para-block input-math"   style="line-adjust:0"><img src="" alt="\[Init = (\bigwedge_{v_i \in V_s} v_i = sc_i) ~\wedge~ (~\bigwedge_{v_i \in V_c} v_i = c_i)\]" class="math-display math" style="vertical-align:-0.000em;height:2.420em"></div></div>
<p>Thus, we see that the initial value of every input variable is characterized by 
a symbolic constant <img src="" alt="$sc_i$" class="math-inline math" style="vertical-align:-0.161em;height:0.624em"> or constant <img src="" alt="$c_i$" class="math-inline math" style="vertical-align:-0.161em;height:0.624em">.  We assume that every non-input
variable in the program is initialized before being used.
</p>
<p class="indent">The strongest postcondition is formulated to deal with open programs,
programs in which some variables are used before being assigned to. 
This surfaces in Rule (1) for assignment, which uses existential quantification
to refer to the value of variable <img src="" alt="$x$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> in the pre-state.
</p>
<p class="indent para-continue">By construction,
we have that every variable is defined before being used.  This means
that the precondition <img src="" alt="$P$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> can be reformulated as a pair <img src="" alt="$&lt;\sigma,P_c&gt;$" class="math-inline math" style="vertical-align:-0.207em;height:0.937em">,
where <img src="" alt="$t$" class="math-inline math" style="vertical-align:-0.000em;height:0.676em"> is a store mapping variables to values and <img src="" alt="$P_c$" class="math-inline math" style="vertical-align:-0.159em;height:0.885em"> is
the path-condition, a list of symbolic expressions (predicates) 
corresponding
to the expressions <img src="" alt="$E$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> evaluated in the context of an <strong>if-then-else</strong> 
statement. Initially, we have that :
</p>
<div class="equation align-center para-block" style="line-adjust:0"><span class="equation-before"><span class="equation-label">(2)</span></span>

<div class="math para-block input-math"   style="line-adjust:0"><img src="" alt="\[\sigma = \{ (v_i,sc_i) | v_i \in V_s \} \cup \{ (v_i,c_i) | v_i \in V_c \}\]" class="math-display math" style="vertical-align:-0.000em;height:1.119em"></div></div>
<p class="para-continue">representing the initial condition <img src="" alt="$Init$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">, and <img src="" alt="$P_c = []$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">, the empty list.
We use <img src="" alt="$\sigma&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em"> to refer to the formula that the store <img src="" alt="$\sigma$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">
induces: 
</p>
<div class="equation align-center para-block" style="line-adjust:0"><span class="equation-before"><span class="equation-label">(3)</span></span>

<div class="math para-block input-math"   style="line-adjust:0"><img src="" alt="\[\sigma &#39; =  \bigwedge_{(v,V) \in \sigma} (v = V)\]" class="math-display math" style="vertical-align:-0.000em;height:2.550em"></div></div>
<p>Thus, the pair <img src="" alt="$&lt;\sigma,P_c&gt;$" class="math-inline math" style="vertical-align:-0.207em;height:0.937em"> represents the predicate 
<img src="" alt="$P = \sigma&#39; \wedge (\bigwedge_{c \in P_c} c)$" class="math-inline math" style="vertical-align:-0.434em;height:1.249em">.
A store <img src="" alt="$\sigma$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> supports two operations: <img src="" alt="$\sigma[x]$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em"> which denotes the
value that <img src="" alt="$x$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> maps to under <img src="" alt="$\sigma$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">; <img src="" alt="$\sigma[x \mapsto V]$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">, which 
produces a new store in which <img src="" alt="$x$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> maps to value <img src="" alt="$V$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> and is everywhere 
else the same as <img src="" alt="$\sigma$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">. 
</p>
<p class="indent para-continue">Now, we can redefine strongest postcondition for assignment to eliminate the
use of existential quantification and model the operation of an interpreter,
by separating out the notion of the store:
</p>
<div class="mathpre para-block input-mathpre"><img src="" alt="\[\begin{mdMathprearray}%
1.\mdMathspace{1}&amp;\mdMathspace{1}\mathid{SP}(&lt;\sigma,\mdMathspace{1}\mathid{P}_\mathid{c}&gt;,\mdMathspace{1}\mathid{x}\mdMathspace{1}:=\mdMathspace{1}\mathid{E})\mdMathspace{1}{~\buildrel\triangle\over=~}\mdMathspace{1}&lt;\sigma[\mathid{x}\mdMathspace{1}\mapsto \mathid{eval}(\sigma,\mathid{E})],\mdMathspace{1}\mathid{P}_\mathid{c}&gt;\\
\end{mdMathprearray}\]" class="math-display math" style="vertical-align:-0.000em;height:1.509em"></div>
<p>where <img src="" alt="$eval(\sigma,E)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em"> evaluates expression <img src="" alt="$E$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> under the store <img src="" alt="$\sigma$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">
(where every occurrence of a free variable
<img src="" alt="$v$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> in <img src="" alt="$E$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> is replaced by the value <img src="" alt="$\sigma[v]$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">). 
This is the standard substitution rule of a standard operational semantics. 
</p>
<p class="indent para-continue">We also redefine the rule for the <strong>if-then-else</strong> statement so
that it chooses which branch to take and appends the appropriate
symbolic expression (predicate) to the path-condition <img src="" alt="$P_c$" class="math-inline math" style="vertical-align:-0.159em;height:0.885em">:
</p>
<div class="mathpre para-block input-mathpre"><img src="" alt="\[\begin{mdMathprearray}%
4.\mdMathspace{1}&amp;\mdMathspace{1}\mathid{SP}(&lt;\sigma,\mdMathspace{1}\mathid{P}_\mathid{c}&gt;,\mdMathspace{1}\mathkw{if}\mdMathspace{1}\mathid{E}\mdMathspace{1}\mathkw{then}\mdMathspace{1}\mathid{S}_1\mdMathspace{1}\mathkw{else}\mdMathspace{1}\mathid{S}_2\mdMathspace{1}\mathkw{end})\mdMathspace{1}{~\buildrel\triangle\over=~}\mdMathspace{2}\mdMathbr{}
\mdMathindent{3}&amp;\mdMathspace{3}\mathkw{let}\mdMathspace{1}\mathid{choice}\mdMathspace{1}=\mdMathspace{1}\mathid{eval}(\sigma,\mathid{E})\mdMathspace{1}\mathkw{in}\mdMathbr{}
\mdMathindent{3}&amp;\mdMathspace{3}\mathkw{if}\mdMathspace{1}\mathid{choice}\mdMathspace{1}\mathkw{then}\mdMathspace{1}\mathid{SP}(&lt;\sigma,\mdMathspace{1}\mathid{P}_\mathid{c}\mdMathspace{1}::\mdMathspace{1}\mathid{expr}(\mathid{choice})\mdMathspace{1}&gt;,\mathid{S}_1)\mdMathspace{1}\mdMathbr{}
\mdMathindent{3}&amp;\mdMathspace{3}\mathkw{else}\mdMathspace{1}\mathid{SP}(&lt;\sigma,\mdMathspace{1}\mathid{P}_\mathid{c}\mdMathspace{1}::\mdMathspace{1}\neg \mathid{expr}(\mathid{choice})\mdMathspace{1}&gt;,\mathid{S}_2)
\end{mdMathprearray}\]" class="math-display math" style="vertical-align:-0.000em;height:5.386em"></div>
<p>The other strongest postcondition rules remain unchanged.
</p><h3 id="sec-summing-it-up"   style="bookmark:3.3.&#8194;Summing it up"><span class="heading-before"><span class="heading-label">3.3</span>.&#8194;</span>Summing it up</h3>
<p>We have shown how the symbolic predicate transformer <img src="" alt="$SP$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> can 
be refined into an symbolic interpreter operating over the
symbolic types defined in the previous section.
In the case when every input variable is symbolic and every
operator is redefined, the path-condition is equivalent to the
<em>strongest postcondition</em> of the execution path <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em">. 
This guarantees that the path-condition for <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> is <em>sound</em>.
In the case where a subset of the input variables are symbolic
and/or not all operators are redefined, the path-condition of <img src="" alt="$p$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> 
is not guaranteed to be sound. We leave it as an exercise to the
reader to establish sufficient conditions under which the 
use of concrete values in place of symbolic expressions is 
guaranteed to result in sound path-conditions. 
</p>
<p class="indent">This section does not address the compilation of a symbolic
expression to the (logic) language of an underlying ATP, nor the
lifting of a satsifying assignment to a formula back to the
level of the source language. This is best done for a particular
source language and ATP, as detailed in the next section. 
</p><h2 id="sec-impl"   style="bookmark:4.&#8194;Architecture of PyExZ3"><span class="heading-before"><span class="heading-label">4</span>.&#8194;</span>Architecture of PyExZ3</h2>
<p>In this section we present the high-level architecture
of a simple DSE tool for the Python language, written in Python, called&nbsp;<a href="http://www.github.com/thomasjball/pyexz3">PyExZ3</a>. 
Figure&nbsp;<a href="#fig-arch" title="Classes in PyExZ3" class="localref" style="target-element:figure"><span class="figure-label">6</span></a>
shows the class diagram (dashed edges are &#8220;has-a&#8221; relationships; solid edges
are &#8220;is-a&#8221; relationships) of the tool. 
</p>
<figure id="fig-arch" class="figure align-center"    style="page-align:here">
<p data-line="1"><span data-line="1"></span><img src="" title="arch" alt="arch" style="width:100%"><span data-line="1"></span>
</p>
<hr  class="figureline madoko" data-line="2">

<div data-line="3"><span data-line="3"></span><fig-caption class="figure-caption"><span class="caption-before"><strong>Figure&#160;<span class="figure-label">6</span>.</strong> </span>Classes in PyExZ3</fig-caption><span data-line="3"></span>
</div></figure><h3 id="sec-loadingtesting-the-code-under-test"   style="bookmark:4.1.&#8194;Loading/testing the code under test"><span class="heading-before"><span class="heading-label">4.1</span>.&#8194;</span>Loading/testing the code under test</h3>
<p>The <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Loader</span></code> class takes as input the name of a Python file (e.g., <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>foo</span><span class='token delimiter python'>.</span><span class='token identifier python'>py</span></code>) 
to import. The loader expects to find a function named
<code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>foo</span></code> inside the file <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>foo</span><span class='token delimiter python'>.</span><span class='token identifier python'>py</span></code>, which will serve as the starting point
for symbolic execution. Thc <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>FunctionInvocation</span></code> class
wraps this starting point. By default, each parameter to <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>foo</span></code> is
a <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicInteger</span></code> unless there is decorator <code class="code code1 language-python lang-python python highlighted" ><span class='token delimiter python'>@</span><span class='token identifier python'>symbolic</span></code> specifying
the type to use for a particular argument.
</p>
<p class="indent">The loader provides the capability to reload the
file/module <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>foo</span><span class='token delimiter python'>.</span><span class='token identifier python'>py</span></code> so that the function <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>foo</span></code> can be 
reexecuted within the same process from the same initial
state with different inputs (see the class <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>ExplorationEngine</span></code>)
via the <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>FunctionInvocation</span></code> class. 
</p>
<p class="indent">Finally, the loader looks for specially named functions <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>expected_result</span></code>
(<code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>expected_result_set</span></code>) in file <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>foo</span><span class='token delimiter python'>.</span><span class='token identifier python'>py</span></code> to use as a test oracle after
the path exploration (by <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>ExplorationEngine</span></code>) has completed. These
functions are expected to return a list of values to check
against the list of return values collected from the executions of 
the <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>foo</span></code> function.
The presence of the function <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>expected_result</span></code> (<code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>expected_result_set</span></code>) 
yields a comparison of the two lists as bags (sets). We use such weaker
tests, rather than list equality, because the order in which paths
are explored by the <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>ExplorationEngine</span></code> can easily change due to small
differences in the input programs. 
</p><h3 id="sec-symbolic-types"   style="bookmark:4.2.&#8194;Symbolic types"><span class="heading-before"><span class="heading-label">4.2</span>.&#8194;</span>Symbolic types</h3>
<p>Python supports multiple inheritance and, more importantly,
allows user-defined classes to inherit 
from its built-in types (such as <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>object</span></code> and <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>int</span></code>).
We use these two features two implement
symbolic versions of Python objects and integers, 
following the instrumented type approach defined in Section&nbsp;<a href="#sec-semantics" title="2.&#8194;Instrumented Types" class="localref" style="target-element:h1"><span class="heading-label">2</span></a>. 
</p>
<p class="indent">The abstract class <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicType</span></code> contains the 
symbolic expression tree and provides basic functions for constructing 
and accessing the tree.  This class does double duty, as it is used
to represent the (typed) symbolic constants associated with the parameters to the 
function, as well as the expression trees (per Section&nbsp;<a href="#sec-semantics" title="2.&#8194;Instrumented Types" class="localref" style="target-element:h1"><span class="heading-label">2</span></a>). Recall
that the symbolic constants only appear as leaves of expression trees.
This means that the expression tree stored in a <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicType</span></code> will
have instances of a <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicType</span></code> as some of its leaves, namely
those leaves representing the symbolic constants.
<!-- Need to say why this is important -->
The abstract class provides an <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>unwrap</span></code> method which returns
the pair of concrete value and expression tree associated with
the <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicType</span></code>, as well as a <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>wrap</span></code> method that takes a 
pair of concrete value and expression tree and creates a <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicType</span></code>
encapsulating them. 
</p>
<p class="indent">The class <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicObject</span></code> inherits from both <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>object</span></code> and <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicType</span></code> and
overrides the basic comparison operations (<code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__eq__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__neq__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__lt__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__le__</span></code>,
<code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__gt__</span></code>, and <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__ge__</span></code>).
The class <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicInteger</span></code> inherits from both <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>int</span></code> and <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicObject</span></code>
and overrides a number of <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>int</span></code>&#39;s arithmetic methods
(<code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__add__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__sub__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__mul__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__mod__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__floordiv_</span></code>)
and bitwise methods
(<code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__and__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__or__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__xor__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__lshift__</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__rshift__</span></code>).
</p><h3 id="sec-tracing-control-flow"   style="bookmark:4.3.&#8194;Tracing control-flow"><span class="heading-before"><span class="heading-label">4.3</span>.&#8194;</span>Tracing control-flow</h3>
<p>As Python interprets a program, it will evaluate expressions, 
substituting the value of a variable in its place in an 
expression, applying operators (methods) to 
parameter values and assigning the return values of methods
to variables. Value of type <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicInteger</span></code> will simply flow
through this interpretation, without necessitating any change 
to the program or the interpreter. This takes care
of the case of the strongest-postcondition rule for assignment,
as elaborated in Section&nbsp;<a href="#sp-refined" title="3.2.&#8194;From  to DSE" class="localref" style="target-element:h2"><span class="heading-label">3.2</span></a>.
</p>
<p class="indent">The strong-postcondition rule for a conditional test requires
a little more work. In Python, any object can be tested in
an <code class="code code1 language-python lang-python python highlighted" ><span class='token keyword python'>if</span></code> or <code class="code code1 language-python lang-python python highlighted" ><span class='token keyword python'>while</span></code> condition or as the operand of a boolean operation
(<code class="code code1 language-python lang-python python highlighted" ><span class='token keyword python'>and</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token keyword python'>or</span></code>, <code class="code code1 language-python lang-python python highlighted" ><span class='token keyword python'>not</span></code>)
The Python base class <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>object</span></code> provides a method named <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__bool__</span></code> that
the Python runtime calls whenever it needs to perform such a conditional test.
This hook provides us what we need to trace the conditional
control-flow of a Python execution.  We override this method in the class
<code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicObject</span></code> in order to inform the <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>PathToConstraint</span></code> object (defined
later) of the symbolic expression for the conditional (as captured by
the <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicInteger</span></code> subclass). 
</p>
<p class="indent">Note that the use of this hook in combination with the
tainted types will only trace those conditionals
in a Python execution whose values inherit from <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicObject</span></code>; 
by definition, &#8220;untainted&#8221; conditionals do not depend on symbolic 
inputs so there is no value in adding them to the path-condition.
</p><h3 id="sec-recording-path-conditions"   style="bookmark:4.4.&#8194;Recording path-conditions"><span class="heading-before"><span class="heading-label">4.4</span>.&#8194;</span>Recording path-conditions</h3>
<p>A <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Predicate</span></code> records a conditional (more precisly the symbolic expression
found in <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicInteger</span></code>) and
which way it evaluated in an execution.  A <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraint</span></code>
has a <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Predicate</span></code>, a parent <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraint</span></code> and a set
of <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraint</span></code> children. <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraints</span></code> form a tree, where
each path starting from the root of the tree represents
a path-condition. The tree represents all path-conditions that have
been explored so far.
</p>
<p class="indent">The class <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>PathToConstraint</span></code> has a reference to the root of 
the tree of <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraint</span></code>s
and is responsible for installing a new <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraint</span></code> in the tree
when notified by the overrided <code class="code code1 language-python lang-python python highlighted" ><span class='token predefined python'>__bool__</span></code> method of <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicObject</span></code>.
<code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>PathToConstraint</span></code> also tracks whether or not the current execution
is following an existing path in the tree and grows the
tree as needed. In fact, it actually
tracks whether or not the current execution follows a particular
<em>expected path</em> in the tree.
</p>
<p class="indent">The expected path is the result
of the <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>ExplorationEngine</span></code> picking a constraint <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> in the tree,
and asking the ATP if the path-condition consisting of the prefix
of predicates up to but not including <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> in the tree, 
followed by the negation of <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">&#39;s predicate is satisfiable. If the 
ATP returns &#8220;satisfiable&#8221; (with a new input <img src="" alt="$i$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">), then the assumption
is that path-condition prefix is sound (that is, the execution of
the program on input <img src="" alt="$i$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> will follow the prefix). 
</p>
<p class="indent">However, it is possible 
for the path-condition to be unsound and for 
the executed path to diverge early 
from the expected path, due to the fact that not every operation
has a symbolic encoding.  The tool simply reports the divergence
and continues to process the execution as usual (as a diverging
path may lead to some other interesting part of the code). 
</p><h3 id="sec-from-symbolic-types-to-z3"   style="bookmark:4.5.&#8194;From symbolic types to Z3"><span class="heading-before"><span class="heading-label">4.5</span>.&#8194;</span>From symbolic types to Z3</h3>
<p>As we have explained DSE, the symbolic expressions are 
represented at the level of the source language. As detailed later
in Section&nbsp;<a href="#sec-int2z3" title="5.&#8194;From Python Integers to Z3 Arithmetic" class="localref" style="target-element:h1"><span class="heading-label">5</span></a>, we must translate 
from the source language to the input language of an
automated theorem prover (ATP), in this case&nbsp;<a href="http://z3.codeplex.org/">Z3</a>.  This
separation of languages is quite useful, as we may have
the need to translate a given symbolic expression
to the ATP&#39;s language multiple times, to make use of different
features of the underlying ATP. 
Furthermore, this separation
of concerns allows us to easily retarget the DSE tool to a
different ATP. 
</p>
<p class="indent">The base class <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Z3Expression</span></code> represents a Z3 formula. The two 
subclasses <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Z3Integer</span></code> and <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Z3BitVector</span></code> represent different ways 
to model arithmetic reasoning about integers in Z3. We will describe
the details of these encodings in Section&nbsp;<a href="#sec-int2z3" title="5.&#8194;From Python Integers to Z3 Arithmetic" class="localref" style="target-element:h1"><span class="heading-label">5</span></a>.
</p>
<p class="indent">The class <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Z3Wrapper</span></code> is responsible for performing the
translation from the source language (Python) to Z3&#39;s input language, 
invoking Z3, and lifting a Z3 answer back to the level of Python. 
The <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>findCounterexample</span></code> method does all the work, taking as
input a list of <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Predicate</span></code>s (called <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>assertions</span></code>) 
as well as a single <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Predicate</span></code> (called
the <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>query</span></code>). The <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>assertions</span></code> represent a path-condition
prefix derived from the <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraint</span></code> tree that we wish the next
execution to follow, while <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>query</span></code> represents the predicate
following the prefix in the tree that we will negate.
</p>
<p class="indent para-continue">The method constructs the formula
</p>
<div class="equation align-center para-block" style="line-adjust:0"><span class="equation-before"><span class="equation-label">(4)</span></span>

<div class="math para-block input-math"   style="line-adjust:0"><img src="" alt="\[(\bigwedge_{a \in asserts} a) \wedge \neg query\]" class="math-display math" style="vertical-align:-0.000em;height:2.342em"></div></div>
<p>and asks Z3 if it is satisfiable. The method performs
a standard syntactic &#8220;cone of influence&#8221; (CIF)
reduction on the <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>asserts</span></code> with respect to the 
<code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>query</span></code> to shrink the size of the formula. For example,
if <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>asserts</span></code> is the set of predicates <img src="" alt="$\{ (x&lt;a), (a&lt;0), (y&gt;0) \}$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em"> and
the query is <img src="" alt="$(x=0)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">, then the CIF yields the
set  <img src="" alt="$\{ (x&lt;a), (a&lt;0) \}$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">, which does not include the predicate <img src="" alt="$(y&gt;0)$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">,
as the variable <img src="" alt="$y$" class="math-inline math" style="vertical-align:-0.210em;height:0.676em"> is not in the set of variables (transitively)
related to variable <img src="" alt="$x$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">.
</p>
<p class="indent">If the formula is satisfiable a model is requested
from Z3 and lifted back to Python&#39;s type universe.  Note that
because of the CIF reduction, the model may not mention certain
input variables, in which case we simply keep their values from
the execution from which the <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>asserts</span></code> and <code class="code code1 language-python lang-python python highlighted" ><span class='token identifier python'>query</span></code> were derived. 
</p><h3 id="sec-putting-it-all-together"   style="bookmark:4.6.&#8194;Putting it all together"><span class="heading-before"><span class="heading-label">4.6</span>.&#8194;</span>Putting it all together</h3>
<p>The class <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>ExplorationEngine</span></code> ties everything together. It kicks off
an execution of the Python code under test using <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>FunctionInvocation</span></code>.
As the Python code executes, building symbolic expressions via <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>SymbolicType</span></code>
and its subclasses, callbacks to <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>PathToConstraint</span></code> create
a path-condition, represented by <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraint</span></code> and <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Predicate</span></code>. 
Newly discovered <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraints</span></code> are added to the end of a deque maintained by
<code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>ExplorationEngine</span></code>.
</p>
<p class="indent">Given the first seed execution, <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>ExplorationEngine</span></code> starts the work of 
exploring paths in a breadth-first fashion. It removes a <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraint</span></code> <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">
from the front of its deque and, if <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> has not been already &#8220;processed&#8221;, 
uses <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Z3Wrapper</span></code> to find a new input (as discussed in the previous section)
where <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> is the query (to be negated) and the path to <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> in the 
<code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraint</span></code> tree forms the assertions. 
</p>
<p class="indent">A <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Constraint</span></code> <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> in the tree is considered &#8220;processed&#8221; if an execution 
has covered <img src="" alt="$c&#39;$" class="math-inline math" style="vertical-align:-0.000em;height:0.833em">, a sibling of <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em"> in the tree that represents
the negation of the predicate associated with <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">, or if constraint <img src="" alt="$c$" class="math-inline math" style="vertical-align:-0.000em;height:0.468em">
has been removed from the deque. 
</p><h2 id="sec-int2z3"   style="bookmark:5.&#8194;From Python Integers to Z3 Arithmetic"><span class="heading-before"><span class="heading-label">5</span>.&#8194;</span>From Python Integers to Z3 Arithmetic</h2>
<p>In languages such as C and Java, integers are finite-precision,
generally limited to the size of a machine word (32 or 64 bits, for example).
For such languages, satisfiability of finite-precision integer arithmetic
is decidable and can be reduced to Z3&#39;s theory of bit-vectors, where
each arithmetic operation is encoded by a circuit. This translation permits 
reasoning about non-linear arithmetic problems, such as 
<img src="" alt="$\exists x,y,z : x*z + y \leq (z/y)+5$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em">.
</p>
<p class="indent">Python (3.0) integers, however, are not finite-precision. They are only
limited by the size of machine memory. This means, for example, that
Python integers don&#39;t overflow or underflow. It also means that
we can&#39;t hope to decide algorithmically whether or not a given
equation over integer variables has a solution in general. Hibert&#39;s famous
10th problem and its solution by Matiyasevich tells us that it is
undecidable whether or not a polynomial
equation of the form <img src="" alt="$p(x_1, \ldots, x_n) = 0$" class="math-inline math" style="vertical-align:-0.280em;height:1.119em"> with integer coefficients
has an solution in the integers.
</p>
<p class="indent">This means that we will resort to heuristic approaches in our use
of the&nbsp;<a href="http://z3.codeplex.org/">Z3</a> ATP.  The special case of linear integer arithmetic (LIA)
is decidable and supported by Z3. In order to deal with non-linear operations,
we use uninterpreted functions (UF). Thus, if Z3 returns
&#8220;unsatisfiable&#8221; we know that there is no solution, but if the
Z3 &#8220;satisfiable&#8221;, we must treat the answer as a &#8220;don&#39;t know&#8221;. 
The class <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Z3Integer</span></code> is used to translate a symbolic expression
into the theory LIA+UF and check for unsatisfiability. We leave it as an
implementation exercise to check if a symbolic expression can
be converted to LIA (without the use of UF) in order to make
use of &#8220;satisfiable&#8221; answers from the LIA solver.
</p>
<p class="indent">If the translation to <code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Z3Integer</span></code> does not return &#8220;unsatisfiable&#8221;, we
use Z3&#39;s bit vector decision procedure (via the class
<code class="code code1 language-python lang-python python highlighted" ><span class='token namespace identifier python'>Z3BitVector</span></code>) to heuristically
try to find satisfiable answers, even in the presence of non-linear 
arithmetic. We start with bitvectors of size <img src="" alt="$N=32$" class="math-inline math" style="vertical-align:-0.000em;height:0.754em"> and <em>bound</em> the values
of the symbolic constants to fit within 8 bits in order to find 
satisfiable solutions
with small values. Also, because Python integers do not overflow/underflow, 
the bound helps us reserve space in the bitvector to allow the
results of operations to exceed the bound while not overflowing
the bitvector. As long as Z3 returns &#8220;unsatisfiable&#8221; we increase
the bound. If the bound reaches <img src="" alt="$N$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">, we increase <img src="" alt="$N$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> by 8 bits,
leaving the bound where it is and continue. 
</p>
<p class="indent">If Z3 returns
&#8220;satisfiable&#8221;, it may be the case that Z3 found a solution
that involved overflow in the bitvector world of arithemetic
(modulo <img src="" alt="$2^N-1$" class="math-inline math" style="vertical-align:-0.084em;height:0.937em">). Therefore,
the solution is validated back in the
Python world by evaluating the formula under that solution
using Python semantics. 
If the formula does not evaluate to the same
value in both worlds, then we increase <img src="" alt="$N$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em"> by 8 bits (to 
create a gap between the bound and <img src="" alt="$N$" class="math-inline math" style="vertical-align:-0.000em;height:0.728em">) and continue to search
for a solution.
</p>
<p class="indent">The process terminates when we find a valid satisfying solution 
or <img src="" alt="$N=64$" class="math-inline math" style="vertical-align:-0.000em;height:0.781em"> and the bound reaches 64 (in which case, we return &#8220;don&#39;t know&#8221;).
</p><h2 id="sec-extensions"   style="bookmark:6.&#8194;Extensions"><span class="heading-before"><span class="heading-label">6</span>.&#8194;</span>Extensions</h2>
<p>We have presented the basics of dynamic symbolic execution 
(for Python).
A more thorough treatment would deal with other data types besides
integers, such as Python dictionaries, strings and lists, each
of which presents their own challenges for symbolic reasoning. 
There are many other interesting challenges in DSE, such
as dealing with user-defined classes (rather than built-in types
as done here) and multi-threaded execution. 
</p><h2 id="sec-acknowledgements"   style="bookmark:7.&#8194;Acknowledgements"><span class="heading-before"><span class="heading-label">7</span>.&#8194;</span>Acknowledgements</h2>
<p>Many thanks to the students of the 2014 Marktoberdorf Summer School
on Dependable Software Systems Engineering
for their questions and feedback about the first author&#39;s lectures on dynamic
symbolic execution. The following students of the summer school
helpfully provided tests for the&nbsp;<a href="http://www.github.com/thomasjball/pyexz3">PyExZ3</a> tool: Daniel Darvas,
Damien Rusinek, Christian Dehnert and Thomas Pani. Thanks also to Peter
Chapman for his contributions. 
</p><!-- 
# From Python Dictionaries to Z3 Maps { #sec-dict2z3 }

Python dictionaries, which map keys to values,
introduce mutation into the picture. The methods are:

- Length:     `__length__(self)` - will be maintained concretely, as cardinality constraints
are beyond the scope of what we can handle
- Get:     `__getitem__(self,key)` - Select
- Set:     `__setitem__(self,key,value)` - Update
- Lookup:     `__contains__(self,key)` - 
- Delete:     `__delitem__(self,key)` - Update 


A dictionary can be mutated via the `__setitem__` and '__delitem__` methods.
The keys stored  in Python dictionary must be hashable values. 
All of Python's immutable
built-in objects (such as integers, tuples and strings) are hashable. 
User-defined classes give rise to hashable mutable objects, where
the hash value is the object id (an immutable field of the object).

Ideally, symbolic expression trees should contain only
immutable values, as they are a pure function of the initial
(immutable) state of a program.  However, the reality is that
the values associated with keys in a dictionary can be mutable.
For example, a dictionary itself can be a value in another
dictionary.    

As we will see, for the purposes of modelling a dictionary symbolically, 
however, the object id of the value in a (key,value) pair is all that
needs to be recorded. The object id is immutable, as mentioned before. 
Thus, we can represent the state of the dictionary via an append-only log 
of updates where the parameters 
to each update are immutable values (set and delete are the update
operations).  Each lookup/get/length operation hangs off of a particular
prefix of the log. 

We model the dictionary as initially
empty, containing no mapping (rejects all lookups and get, length is zero).



The essential axioms

* Initially empty
* Select
* Update

Inverting select means that we need disequality on values in
the dictionary (SymbolicObject)

Equality of dictionaries (extensional arrays)

-->

<h2 id="sec-references" >References</h2>
<div class="tex input-tex">
<div class="bibliography bib-numeric"   data-line="1" style="bibstyle:plainnat">

<div id="cadare05" class="bibitem"   data-line="4" style="searchterm:Cristian+Cadar+Dawson+Engler+Execution+generated+test+cases+make+systems+code+crash+itself+_Proceedings+International+SPIN+Workshop_+pages++"><span data-line="5"></span><span class="bibitem-before">[<span class="bibitem-label">1</span>]&#160;&#160;</span><span data-line="5"></span>Cristian Cadar and Dawson<span data-line="5"></span>&#160;<span data-line="5"></span>R. Engler.
<span data-line="6"></span><span class="newblock"></span><span data-line="6"></span> Execution generated test cases: How to make systems code crash
  itself.
<span data-line="8"></span><span class="newblock"></span><span data-line="8"></span> In <span data-line="8"></span><em>Proceedings of 12th International SPIN Workshop</em><span data-line="8"></span>, pages
  2<span data-line="9"></span>&#8211;<span data-line="9"></span>23, 2005.<span data-line="9"></span>&nbsp;<a href="http://www.bing.com/search?q=Cristian+Cadar+Dawson+Engler+Execution+generated+test+cases+make+systems+code+crash+itself+_Proceedings+International+SPIN+Workshop_+pages++" class="bibsearch">&#128270;</a></div>
<div id="cadars13" class="bibitem"   data-line="12" style="searchterm:Symbolic+execution+software+testing+three+decades+later++Cristian+Cadar+Koushik+"><span data-line="13"></span><span class="bibitem-before">[<span class="bibitem-label">2</span>]&#160;&#160;</span><span data-line="13"></span>Cristian Cadar and Koushik Sen.
<span data-line="14"></span><span class="newblock"></span><span data-line="14"></span> Symbolic execution for software testing: three decades later.
<span data-line="15"></span><span class="newblock"></span><span data-line="15"></span> <span data-line="15"></span><em>Communications of the ACM</em><span data-line="15"></span>, 56<span data-line="15"></span><span style="penalty:0"></span><span data-line="15"></span> (2):<span data-line="15"></span><span style="penalty:0"></span><span data-line="15"></span> 82<span data-line="15"></span>&#8211;<span data-line="15"></span>90,
  2013.<span data-line="16"></span>&nbsp;<a href="http://www.bing.com/search?q=Symbolic+execution+software+testing+three+decades+later++Cristian+Cadar+Koushik+" class="bibsearch">&#128270;</a></div>
<div id="cadargpde06" class="bibitem"   data-line="19" style="searchterm:Cristian+Cadar+Vijay+Ganesh+Peter+Pawlowski+David+Dill+Dawson+Engler+automatically+generating+inputs+death+_Proceedings+Conference+Computer+Communications+Security_+pages++"><span data-line="20"></span><span class="bibitem-before">[<span class="bibitem-label">3</span>]&#160;&#160;</span><span data-line="20"></span>Cristian Cadar, Vijay Ganesh, Peter<span data-line="20"></span>&#160;<span data-line="20"></span>M. Pawlowski, David<span data-line="20"></span>&#160;<span data-line="20"></span>L. Dill, and Dawson<span data-line="20"></span>&#160;<span data-line="20"></span>R.
  Engler.
<span data-line="22"></span><span class="newblock"></span><span data-line="22"></span> EXE: automatically generating inputs of death.
<span data-line="23"></span><span class="newblock"></span><span data-line="23"></span> In <span data-line="23"></span><em>Proceedings of the 13th ACM Conference on Computer and
  Communications Security</em><span data-line="24"></span>, pages 322<span data-line="24"></span>&#8211;<span data-line="24"></span>335, 2006.<span data-line="24"></span>&nbsp;<a href="http://www.bing.com/search?q=Cristian+Cadar+Vijay+Ganesh+Peter+Pawlowski+David+Dill+Dawson+Engler+automatically+generating+inputs+death+_Proceedings+Conference+Computer+Communications+Security_+pages++" class="bibsearch">&#128270;</a></div>
<div id="clarke76" class="bibitem"   data-line="27" style="searchterm:+system+generate+test+data+symbolically+execute+programs++Lori+Clarke+"><span data-line="28"></span><span class="bibitem-before">[<span class="bibitem-label">4</span>]&#160;&#160;</span><span data-line="28"></span>Lori<span data-line="28"></span>&#160;<span data-line="28"></span>A. Clarke.
<span data-line="29"></span><span class="newblock"></span><span data-line="29"></span> A system to generate test data and symbolically execute programs.
<span data-line="30"></span><span class="newblock"></span><span data-line="30"></span> <span data-line="30"></span><em>IEEE Transactions on Software Engineering</em><span data-line="30"></span>, 2<span data-line="30"></span><span style="penalty:0"></span><span data-line="30"></span>
  (3):<span data-line="31"></span><span style="penalty:0"></span><span data-line="31"></span> 215<span data-line="31"></span>&#8211;<span data-line="31"></span>222, 1976.<span data-line="31"></span>&nbsp;<a href="http://www.bing.com/search?q=+system+generate+test+data+symbolically+execute+programs++Lori+Clarke+" class="bibsearch">&#128270;</a></div>
<div id="demourab08" class="bibitem"   data-line="34" style="searchterm:+efficient+solver++Leonardo+Mendon+Moura+Nikolaj+rner+"><span data-line="35"></span><span class="bibitem-before">[<span class="bibitem-label">5</span>]&#160;&#160;</span><span data-line="35"></span>Leonardo<span data-line="35"></span>&#160;<span data-line="35"></span>Mendon<span data-line="35"></span>&#231;<span data-line="35"></span>a de<span data-line="35"></span>&#160;<span data-line="35"></span>Moura and Nikolaj Bj<span data-line="35"></span>&#248;<span data-line="35"></span>rner.
<span data-line="36"></span><span class="newblock"></span><span data-line="36"></span> Z3: an efficient SMT solver.
<span data-line="37"></span><span class="newblock"></span><span data-line="37"></span> In <span data-line="37"></span><em>Proceedings of the 14th International Conference of Tools
  and Algorithms for the Construction and Analysis of Systems</em><span data-line="38"></span>, pages 337<span data-line="38"></span>&#8211;<span data-line="38"></span>340,
  2008.<span data-line="39"></span>&nbsp;<a href="http://www.bing.com/search?q=+efficient+solver++Leonardo+Mendon+Moura+Nikolaj+rner+" class="bibsearch">&#128270;</a></div>
<div id="dijkstra76" class="bibitem"   data-line="42" style="searchterm:+Discipline+Programming_++Edsger+Dijkstra+"><span data-line="43"></span><span class="bibitem-before">[<span class="bibitem-label">6</span>]&#160;&#160;</span><span data-line="43"></span>Edsger<span data-line="43"></span>&#160;<span data-line="43"></span>W. Dijkstra.
<span data-line="44"></span><span class="newblock"></span><span data-line="44"></span> <span data-line="44"></span><em>A Discipline of Programming</em><span data-line="44"></span>.
<span data-line="45"></span><span class="newblock"></span><span data-line="45"></span> Prentice-Hall, 1976.<span data-line="45"></span>&nbsp;<a href="http://www.bing.com/search?q=+Discipline+Programming_++Edsger+Dijkstra+" class="bibsearch">&#128270;</a></div>
<div id="godefroid11" class="bibitem"   data-line="48" style="searchterm:Higher+order+test+generation++Patrice+Godefroid+"><span data-line="49"></span><span class="bibitem-before">[<span class="bibitem-label">7</span>]&#160;&#160;</span><span data-line="49"></span>Patrice Godefroid.
<span data-line="50"></span><span class="newblock"></span><span data-line="50"></span> Higher-order test generation.
<span data-line="51"></span><span class="newblock"></span><span data-line="51"></span> In <span data-line="51"></span><em>Proceedings of the ACM SIGPLAN Conference on Programming
  Language Design and Implementation</em><span data-line="52"></span>, pages 258<span data-line="52"></span>&#8211;<span data-line="52"></span>269, 2011.<span data-line="52"></span>&nbsp;<a href="http://www.bing.com/search?q=Higher+order+test+generation++Patrice+Godefroid+" class="bibsearch">&#128270;</a></div>
<div id="godefroidks05" class="bibitem"   data-line="55" style="searchterm:DART+directed+automated+random+testing++Patrice+Godefroid+Nils+Klarlund+Koushik+"><span data-line="56"></span><span class="bibitem-before">[<span class="bibitem-label">8</span>]&#160;&#160;</span><span data-line="56"></span>Patrice Godefroid, Nils Klarlund, and Koushik Sen.
<span data-line="57"></span><span class="newblock"></span><span data-line="57"></span> DART: directed automated random testing.
<span data-line="58"></span><span class="newblock"></span><span data-line="58"></span> In <span data-line="58"></span><em>Proceedings of the ACM SIGPLAN Conference on Programming
  Language Design and Implementation</em><span data-line="59"></span>, pages 213<span data-line="59"></span>&#8211;<span data-line="59"></span>223, 2005.<span data-line="59"></span>&nbsp;<a href="http://www.bing.com/search?q=DART+directed+automated+random+testing++Patrice+Godefroid+Nils+Klarlund+Koushik+" class="bibsearch">&#128270;</a></div>
<div id="godefroidlm12" class="bibitem"   data-line="62" style="searchterm:SAGE+whitebox+fuzzing+security+testing++Patrice+Godefroid+Michael+Levin+David+Molnar+"><span data-line="63"></span><span class="bibitem-before">[<span class="bibitem-label">9</span>]&#160;&#160;</span><span data-line="63"></span>Patrice Godefroid, Michael<span data-line="63"></span>&#160;<span data-line="63"></span>Y. Levin, and David<span data-line="63"></span>&#160;<span data-line="63"></span>A. Molnar.
<span data-line="64"></span><span class="newblock"></span><span data-line="64"></span> SAGE: whitebox fuzzing for security testing.
<span data-line="65"></span><span class="newblock"></span><span data-line="65"></span> <span data-line="65"></span><em>Communications of the ACM</em><span data-line="65"></span>, 55<span data-line="65"></span><span style="penalty:0"></span><span data-line="65"></span> (3):<span data-line="65"></span><span style="penalty:0"></span><span data-line="65"></span> 40<span data-line="65"></span>&#8211;<span data-line="65"></span>44,
  2012.<span data-line="66"></span>&nbsp;<a href="http://www.bing.com/search?q=SAGE+whitebox+fuzzing+security+testing++Patrice+Godefroid+Michael+Levin+David+Molnar+" class="bibsearch">&#128270;</a></div>
<div id="gupta00" class="bibitem"   data-line="69" style="searchterm:Generating+test+data+branch+coverage++Neelam+Gupta+Aditya+Mathur+Mary+Soffa+"><span data-line="70"></span><span class="bibitem-before">[<span class="bibitem-label">10</span>]&#160;&#160;</span><span data-line="70"></span>Neelam Gupta, Aditya<span data-line="70"></span>&#160;<span data-line="70"></span>P. Mathur, and Mary<span data-line="70"></span>&#160;<span data-line="70"></span>Lou Soffa.
<span data-line="71"></span><span class="newblock"></span><span data-line="71"></span> Generating test data for branch coverage.
<span data-line="72"></span><span class="newblock"></span><span data-line="72"></span> In <span data-line="72"></span><em>Proceedings of the Automate Software Engineering
  Conference</em><span data-line="73"></span>, pages 219<span data-line="73"></span>&#8211;<span data-line="73"></span>228, 2000.<span data-line="73"></span>&nbsp;<a href="http://www.bing.com/search?q=Generating+test+data+branch+coverage++Neelam+Gupta+Aditya+Mathur+Mary+Soffa+" class="bibsearch">&#128270;</a></div>
<div id="king76" class="bibitem"   data-line="76" style="searchterm:Symbolic+execution+program+testing++James+King+"><span data-line="77"></span><span class="bibitem-before">[<span class="bibitem-label">11</span>]&#160;&#160;</span><span data-line="77"></span>James<span data-line="77"></span>&#160;<span data-line="77"></span>C. King.
<span data-line="78"></span><span class="newblock"></span><span data-line="78"></span> Symbolic execution and program testing.
<span data-line="79"></span><span class="newblock"></span><span data-line="79"></span> <span data-line="79"></span><em>Communications of the ACM</em><span data-line="79"></span>, 19<span data-line="79"></span><span style="penalty:0"></span><span data-line="79"></span> (7):<span data-line="79"></span><span style="penalty:0"></span><span data-line="79"></span>
  385–394, 1976.<span data-line="80"></span>&nbsp;<a href="http://www.bing.com/search?q=Symbolic+execution+program+testing++James+King+" class="bibsearch">&#128270;</a></div>
<div id="korel90" class="bibitem"   data-line="83" style="searchterm:Automated+software+test+data+generation++Bogdan+Korel+"><span data-line="84"></span><span class="bibitem-before">[<span class="bibitem-label">12</span>]&#160;&#160;</span><span data-line="84"></span>Bogdan Korel.
<span data-line="85"></span><span class="newblock"></span><span data-line="85"></span> Automated software test data generation.
<span data-line="86"></span><span class="newblock"></span><span data-line="86"></span> <span data-line="86"></span><em>IEEE Transactions on Software Engineering</em><span data-line="86"></span>, 16<span data-line="86"></span><span style="penalty:0"></span><span data-line="86"></span>
  (8):<span data-line="87"></span><span style="penalty:0"></span><span data-line="87"></span> 870<span data-line="87"></span>&#8211;<span data-line="87"></span>879, 1990.<span data-line="87"></span>&nbsp;<a href="http://www.bing.com/search?q=Automated+software+test+data+generation++Bogdan+Korel+" class="bibsearch">&#128270;</a></div>
<div id="korel92" class="bibitem"   data-line="90" style="searchterm:Dynamic+method+software+test+data+generation++Bogdan+Korel+"><span data-line="91"></span><span class="bibitem-before">[<span class="bibitem-label">13</span>]&#160;&#160;</span><span data-line="91"></span>Bogdan Korel.
<span data-line="92"></span><span class="newblock"></span><span data-line="92"></span> Dynamic method of software test data generation.
<span data-line="93"></span><span class="newblock"></span><span data-line="93"></span> <span data-line="93"></span><em>Journal of Software Testing, Verification and Reliability</em><span data-line="93"></span>,
  2<span data-line="94"></span><span style="penalty:0"></span><span data-line="94"></span> (4):<span data-line="94"></span><span style="penalty:0"></span><span data-line="94"></span> 203<span data-line="94"></span>&#8211;<span data-line="94"></span>213, 1992.<span data-line="94"></span>&nbsp;<a href="http://www.bing.com/search?q=Dynamic+method+software+test+data+generation++Bogdan+Korel+" class="bibsearch">&#128270;</a></div>
<div id="senacav06" class="bibitem"   data-line="97" style="searchterm:Koushik+Agha+CUTE+jcute+Concolic+unit+testing+explicit+path+model+checking+tools+_Proceedings+Computer+Aided+Verification+Conference_+pages++"><span data-line="98"></span><span class="bibitem-before">[<span class="bibitem-label">14</span>]&#160;&#160;</span><span data-line="98"></span>Koushik Sen and Gul Agha.
<span data-line="99"></span><span class="newblock"></span><span data-line="99"></span> CUTE and jcute: Concolic unit testing and explicit path
  model-checking tools.
<span data-line="101"></span><span class="newblock"></span><span data-line="101"></span> In <span data-line="101"></span><em>Proceedings of 18th Computer Aided Verification Conference</em><span data-line="101"></span>,
  pages 419<span data-line="102"></span>&#8211;<span data-line="102"></span>423, 2006.<span data-line="102"></span>&nbsp;<a href="http://www.bing.com/search?q=Koushik+Agha+CUTE+jcute+Concolic+unit+testing+explicit+path+model+checking+tools+_Proceedings+Computer+Aided+Verification+Conference_+pages++" class="bibsearch">&#128270;</a></div></div></div>
<div class="madokologo block" style="text-align:right;font-size:xx-small;margin-top:4em"><span data-line="1"></span>Created with&nbsp;<a href="https://www.madoko.net">Madoko.net</a>.</div>
</body>

</html>
